In the following example, x can appear in ps. However, since it is bounded
(see step 1), this does not pose an issue.
1::nfrab1 |- F/_ x { x e. RR | x < 5 }
2:1:nfel2 |- F/ x A e. { x e. RR | x < 5 }
3::eleq1 |- ( x = A -> ( x e. { x e. RR | x < 5 } <-> A e. { x
e. RR | x < 5 } ) )
qed:2,3:rspc |- ( A e. V -> ( A. x e. V x e. { x e. RR | x < 5 } -> A
e. { x e. RR | x < 5 } ) )
$= ( cv c5 clt wbr cr crab wcel nfrab1 nfel2 eleq1 rspc )
ADZOEFGZAHIZJBQJABCAB
QPAHKLOBQMN $.
$d A x
$d V x
--
You received this message because you are subscribed to the Google Groups
"Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to [email protected].
To view this discussion visit
https://groups.google.com/d/msgid/metamath/92a156a3-0dc0-40c4-8724-1c76a86ff95fn%40googlegroups.com.
