Step |
Hyp |
Ref |
Expression |
1 |
|
rmo3f.1 |
|- F/_ x A |
2 |
|
rmo3f.2 |
|- F/_ y A |
3 |
|
rmo3f.3 |
|- F/ y ph |
4 |
|
df-rmo |
|- ( E* x e. A ph <-> E* x ( x e. A /\ ph ) ) |
5 |
|
sban |
|- ( [ y / x ] ( x e. A /\ ph ) <-> ( [ y / x ] x e. A /\ [ y / x ] ph ) ) |
6 |
1
|
clelsb1fw |
|- ( [ y / x ] x e. A <-> y e. A ) |
7 |
5 6
|
bianbi |
|- ( [ y / x ] ( x e. A /\ ph ) <-> ( y e. A /\ [ y / x ] ph ) ) |
8 |
7
|
anbi2i |
|- ( ( ( x e. A /\ ph ) /\ [ y / x ] ( x e. A /\ ph ) ) <-> ( ( x e. A /\ ph ) /\ ( y e. A /\ [ y / x ] ph ) ) ) |
9 |
|
an4 |
|- ( ( ( x e. A /\ ph ) /\ ( y e. A /\ [ y / x ] ph ) ) <-> ( ( x e. A /\ y e. A ) /\ ( ph /\ [ y / x ] ph ) ) ) |
10 |
|
ancom |
|- ( ( x e. A /\ y e. A ) <-> ( y e. A /\ x e. A ) ) |
11 |
10
|
anbi1i |
|- ( ( ( x e. A /\ y e. A ) /\ ( ph /\ [ y / x ] ph ) ) <-> ( ( y e. A /\ x e. A ) /\ ( ph /\ [ y / x ] ph ) ) ) |
12 |
8 9 11
|
3bitri |
|- ( ( ( x e. A /\ ph ) /\ [ y / x ] ( x e. A /\ ph ) ) <-> ( ( y e. A /\ x e. A ) /\ ( ph /\ [ y / x ] ph ) ) ) |
13 |
12
|
imbi1i |
|- ( ( ( ( x e. A /\ ph ) /\ [ y / x ] ( x e. A /\ ph ) ) -> x = y ) <-> ( ( ( y e. A /\ x e. A ) /\ ( ph /\ [ y / x ] ph ) ) -> x = y ) ) |
14 |
|
impexp |
|- ( ( ( ( y e. A /\ x e. A ) /\ ( ph /\ [ y / x ] ph ) ) -> x = y ) <-> ( ( y e. A /\ x e. A ) -> ( ( ph /\ [ y / x ] ph ) -> x = y ) ) ) |
15 |
|
impexp |
|- ( ( ( y e. A /\ x e. A ) -> ( ( ph /\ [ y / x ] ph ) -> x = y ) ) <-> ( y e. A -> ( x e. A -> ( ( ph /\ [ y / x ] ph ) -> x = y ) ) ) ) |
16 |
13 14 15
|
3bitri |
|- ( ( ( ( x e. A /\ ph ) /\ [ y / x ] ( x e. A /\ ph ) ) -> x = y ) <-> ( y e. A -> ( x e. A -> ( ( ph /\ [ y / x ] ph ) -> x = y ) ) ) ) |
17 |
16
|
albii |
|- ( A. y ( ( ( x e. A /\ ph ) /\ [ y / x ] ( x e. A /\ ph ) ) -> x = y ) <-> A. y ( y e. A -> ( x e. A -> ( ( ph /\ [ y / x ] ph ) -> x = y ) ) ) ) |
18 |
|
df-ral |
|- ( A. y e. A ( x e. A -> ( ( ph /\ [ y / x ] ph ) -> x = y ) ) <-> A. y ( y e. A -> ( x e. A -> ( ( ph /\ [ y / x ] ph ) -> x = y ) ) ) ) |
19 |
2
|
nfcri |
|- F/ y x e. A |
20 |
19
|
r19.21 |
|- ( A. y e. A ( x e. A -> ( ( ph /\ [ y / x ] ph ) -> x = y ) ) <-> ( x e. A -> A. y e. A ( ( ph /\ [ y / x ] ph ) -> x = y ) ) ) |
21 |
17 18 20
|
3bitr2i |
|- ( A. y ( ( ( x e. A /\ ph ) /\ [ y / x ] ( x e. A /\ ph ) ) -> x = y ) <-> ( x e. A -> A. y e. A ( ( ph /\ [ y / x ] ph ) -> x = y ) ) ) |
22 |
21
|
albii |
|- ( A. x A. y ( ( ( x e. A /\ ph ) /\ [ y / x ] ( x e. A /\ ph ) ) -> x = y ) <-> A. x ( x e. A -> A. y e. A ( ( ph /\ [ y / x ] ph ) -> x = y ) ) ) |
23 |
19 3
|
nfan |
|- F/ y ( x e. A /\ ph ) |
24 |
23
|
mo3 |
|- ( E* x ( x e. A /\ ph ) <-> A. x A. y ( ( ( x e. A /\ ph ) /\ [ y / x ] ( x e. A /\ ph ) ) -> x = y ) ) |
25 |
|
df-ral |
|- ( A. x e. A A. y e. A ( ( ph /\ [ y / x ] ph ) -> x = y ) <-> A. x ( x e. A -> A. y e. A ( ( ph /\ [ y / x ] ph ) -> x = y ) ) ) |
26 |
22 24 25
|
3bitr4i |
|- ( E* x ( x e. A /\ ph ) <-> A. x e. A A. y e. A ( ( ph /\ [ y / x ] ph ) -> x = y ) ) |
27 |
4 26
|
bitri |
|- ( E* x e. A ph <-> A. x e. A A. y e. A ( ( ph /\ [ y / x ] ph ) -> x = y ) ) |