Step |
Hyp |
Ref |
Expression |
1 |
|
nfiotad.1 |
|- F/ y ph |
2 |
|
nfiotad.2 |
|- ( ph -> F/ x ps ) |
3 |
|
dfiota2 |
|- ( iota y ps ) = U. { z | A. y ( ps <-> y = z ) } |
4 |
|
nfv |
|- F/ z ph |
5 |
2
|
adantr |
|- ( ( ph /\ -. A. x x = y ) -> F/ x ps ) |
6 |
|
nfeqf1 |
|- ( -. A. x x = y -> F/ x y = z ) |
7 |
6
|
adantl |
|- ( ( ph /\ -. A. x x = y ) -> F/ x y = z ) |
8 |
5 7
|
nfbid |
|- ( ( ph /\ -. A. x x = y ) -> F/ x ( ps <-> y = z ) ) |
9 |
1 8
|
nfald2 |
|- ( ph -> F/ x A. y ( ps <-> y = z ) ) |
10 |
4 9
|
nfabd |
|- ( ph -> F/_ x { z | A. y ( ps <-> y = z ) } ) |
11 |
10
|
nfunid |
|- ( ph -> F/_ x U. { z | A. y ( ps <-> y = z ) } ) |
12 |
3 11
|
nfcxfrd |
|- ( ph -> F/_ x ( iota y ps ) ) |