Step |
Hyp |
Ref |
Expression |
1 |
|
iota2.1 |
|- ( x = A -> ( ph <-> ps ) ) |
2 |
|
elex |
|- ( A e. B -> A e. _V ) |
3 |
|
simpl |
|- ( ( A e. _V /\ E! x ph ) -> A e. _V ) |
4 |
|
simpr |
|- ( ( A e. _V /\ E! x ph ) -> E! x ph ) |
5 |
1
|
adantl |
|- ( ( ( A e. _V /\ E! x ph ) /\ x = A ) -> ( ph <-> ps ) ) |
6 |
|
nfv |
|- F/ x A e. _V |
7 |
|
nfeu1 |
|- F/ x E! x ph |
8 |
6 7
|
nfan |
|- F/ x ( A e. _V /\ E! x ph ) |
9 |
|
nfvd |
|- ( ( A e. _V /\ E! x ph ) -> F/ x ps ) |
10 |
|
nfcvd |
|- ( ( A e. _V /\ E! x ph ) -> F/_ x A ) |
11 |
3 4 5 8 9 10
|
iota2df |
|- ( ( A e. _V /\ E! x ph ) -> ( ps <-> ( iota x ph ) = A ) ) |
12 |
2 11
|
sylan |
|- ( ( A e. B /\ E! x ph ) -> ( ps <-> ( iota x ph ) = A ) ) |