Step |
Hyp |
Ref |
Expression |
1 |
|
nfriotad.1 |
|- F/ y ph |
2 |
|
nfriotad.2 |
|- ( ph -> F/ x ps ) |
3 |
|
nfriotad.3 |
|- ( ph -> F/_ x A ) |
4 |
|
df-riota |
|- ( iota_ y e. A ps ) = ( iota y ( y e. A /\ ps ) ) |
5 |
|
nfnae |
|- F/ y -. A. x x = y |
6 |
1 5
|
nfan |
|- F/ y ( ph /\ -. A. x x = y ) |
7 |
|
nfcvf |
|- ( -. A. x x = y -> F/_ x y ) |
8 |
7
|
adantl |
|- ( ( ph /\ -. A. x x = y ) -> F/_ x y ) |
9 |
3
|
adantr |
|- ( ( ph /\ -. A. x x = y ) -> F/_ x A ) |
10 |
8 9
|
nfeld |
|- ( ( ph /\ -. A. x x = y ) -> F/ x y e. A ) |
11 |
2
|
adantr |
|- ( ( ph /\ -. A. x x = y ) -> F/ x ps ) |
12 |
10 11
|
nfand |
|- ( ( ph /\ -. A. x x = y ) -> F/ x ( y e. A /\ ps ) ) |
13 |
6 12
|
nfiotad |
|- ( ( ph /\ -. A. x x = y ) -> F/_ x ( iota y ( y e. A /\ ps ) ) ) |
14 |
13
|
ex |
|- ( ph -> ( -. A. x x = y -> F/_ x ( iota y ( y e. A /\ ps ) ) ) ) |
15 |
|
nfiota1 |
|- F/_ y ( iota y ( y e. A /\ ps ) ) |
16 |
|
eqidd |
|- ( A. x x = y -> ( iota y ( y e. A /\ ps ) ) = ( iota y ( y e. A /\ ps ) ) ) |
17 |
16
|
drnfc1 |
|- ( A. x x = y -> ( F/_ x ( iota y ( y e. A /\ ps ) ) <-> F/_ y ( iota y ( y e. A /\ ps ) ) ) ) |
18 |
15 17
|
mpbiri |
|- ( A. x x = y -> F/_ x ( iota y ( y e. A /\ ps ) ) ) |
19 |
14 18
|
pm2.61d2 |
|- ( ph -> F/_ x ( iota y ( y e. A /\ ps ) ) ) |
20 |
4 19
|
nfcxfrd |
|- ( ph -> F/_ x ( iota_ y e. A ps ) ) |