Step |
Hyp |
Ref |
Expression |
1 |
|
iota2df.1 |
|- ( ph -> B e. V ) |
2 |
|
iota2df.2 |
|- ( ph -> E! x ps ) |
3 |
|
iota2df.3 |
|- ( ( ph /\ x = B ) -> ( ps <-> ch ) ) |
4 |
|
iota2df.4 |
|- F/ x ph |
5 |
|
iota2df.5 |
|- ( ph -> F/ x ch ) |
6 |
|
iota2df.6 |
|- ( ph -> F/_ x B ) |
7 |
|
simpr |
|- ( ( ph /\ x = B ) -> x = B ) |
8 |
7
|
eqeq2d |
|- ( ( ph /\ x = B ) -> ( ( iota x ps ) = x <-> ( iota x ps ) = B ) ) |
9 |
3 8
|
bibi12d |
|- ( ( ph /\ x = B ) -> ( ( ps <-> ( iota x ps ) = x ) <-> ( ch <-> ( iota x ps ) = B ) ) ) |
10 |
|
iota1 |
|- ( E! x ps -> ( ps <-> ( iota x ps ) = x ) ) |
11 |
2 10
|
syl |
|- ( ph -> ( ps <-> ( iota x ps ) = x ) ) |
12 |
|
nfiota1 |
|- F/_ x ( iota x ps ) |
13 |
12
|
a1i |
|- ( ph -> F/_ x ( iota x ps ) ) |
14 |
13 6
|
nfeqd |
|- ( ph -> F/ x ( iota x ps ) = B ) |
15 |
5 14
|
nfbid |
|- ( ph -> F/ x ( ch <-> ( iota x ps ) = B ) ) |
16 |
1 9 11 4 6 15
|
vtocldf |
|- ( ph -> ( ch <-> ( iota x ps ) = B ) ) |