Step |
Hyp |
Ref |
Expression |
1 |
|
reu3 |
|- ( E! x e. A E. y e. B ph <-> ( E. x e. A E. y e. B ph /\ E. z e. A A. x e. A ( E. y e. B ph -> x = z ) ) ) |
2 |
|
reu3 |
|- ( E! y e. B E. x e. A ph <-> ( E. y e. B E. x e. A ph /\ E. w e. B A. y e. B ( E. x e. A ph -> y = w ) ) ) |
3 |
1 2
|
anbi12i |
|- ( ( E! x e. A E. y e. B ph /\ E! y e. B E. x e. A ph ) <-> ( ( E. x e. A E. y e. B ph /\ E. z e. A A. x e. A ( E. y e. B ph -> x = z ) ) /\ ( E. y e. B E. x e. A ph /\ E. w e. B A. y e. B ( E. x e. A ph -> y = w ) ) ) ) |
4 |
3
|
a1i |
|- ( ( A =/= (/) /\ B =/= (/) ) -> ( ( E! x e. A E. y e. B ph /\ E! y e. B E. x e. A ph ) <-> ( ( E. x e. A E. y e. B ph /\ E. z e. A A. x e. A ( E. y e. B ph -> x = z ) ) /\ ( E. y e. B E. x e. A ph /\ E. w e. B A. y e. B ( E. x e. A ph -> y = w ) ) ) ) ) |
5 |
|
an4 |
|- ( ( ( E. x e. A E. y e. B ph /\ E. z e. A A. x e. A ( E. y e. B ph -> x = z ) ) /\ ( E. y e. B E. x e. A ph /\ E. w e. B A. y e. B ( E. x e. A ph -> y = w ) ) ) <-> ( ( E. x e. A E. y e. B ph /\ E. y e. B E. x e. A ph ) /\ ( E. z e. A A. x e. A ( E. y e. B ph -> x = z ) /\ E. w e. B A. y e. B ( E. x e. A ph -> y = w ) ) ) ) |
6 |
5
|
a1i |
|- ( ( A =/= (/) /\ B =/= (/) ) -> ( ( ( E. x e. A E. y e. B ph /\ E. z e. A A. x e. A ( E. y e. B ph -> x = z ) ) /\ ( E. y e. B E. x e. A ph /\ E. w e. B A. y e. B ( E. x e. A ph -> y = w ) ) ) <-> ( ( E. x e. A E. y e. B ph /\ E. y e. B E. x e. A ph ) /\ ( E. z e. A A. x e. A ( E. y e. B ph -> x = z ) /\ E. w e. B A. y e. B ( E. x e. A ph -> y = w ) ) ) ) ) |
7 |
|
rexcom |
|- ( E. y e. B E. x e. A ph <-> E. x e. A E. y e. B ph ) |
8 |
7
|
anbi2i |
|- ( ( E. x e. A E. y e. B ph /\ E. y e. B E. x e. A ph ) <-> ( E. x e. A E. y e. B ph /\ E. x e. A E. y e. B ph ) ) |
9 |
|
anidm |
|- ( ( E. x e. A E. y e. B ph /\ E. x e. A E. y e. B ph ) <-> E. x e. A E. y e. B ph ) |
10 |
8 9
|
bitri |
|- ( ( E. x e. A E. y e. B ph /\ E. y e. B E. x e. A ph ) <-> E. x e. A E. y e. B ph ) |
11 |
10
|
a1i |
|- ( ( A =/= (/) /\ B =/= (/) ) -> ( ( E. x e. A E. y e. B ph /\ E. y e. B E. x e. A ph ) <-> E. x e. A E. y e. B ph ) ) |
12 |
|
r19.26 |
|- ( A. x e. A ( A. y e. B ( ph -> x = z ) /\ A. x e. A A. y e. B ( ph -> y = w ) ) <-> ( A. x e. A A. y e. B ( ph -> x = z ) /\ A. x e. A A. x e. A A. y e. B ( ph -> y = w ) ) ) |
13 |
|
nfra1 |
|- F/ x A. x e. A A. y e. B ( ph -> y = w ) |
14 |
13
|
r19.3rz |
|- ( A =/= (/) -> ( A. x e. A A. y e. B ( ph -> y = w ) <-> A. x e. A A. x e. A A. y e. B ( ph -> y = w ) ) ) |
15 |
14
|
bicomd |
|- ( A =/= (/) -> ( A. x e. A A. x e. A A. y e. B ( ph -> y = w ) <-> A. x e. A A. y e. B ( ph -> y = w ) ) ) |
16 |
15
|
adantr |
|- ( ( A =/= (/) /\ B =/= (/) ) -> ( A. x e. A A. x e. A A. y e. B ( ph -> y = w ) <-> A. x e. A A. y e. B ( ph -> y = w ) ) ) |
17 |
16
|
adantr |
|- ( ( ( A =/= (/) /\ B =/= (/) ) /\ ( z e. A /\ w e. B ) ) -> ( A. x e. A A. x e. A A. y e. B ( ph -> y = w ) <-> A. x e. A A. y e. B ( ph -> y = w ) ) ) |
18 |
17
|
anbi2d |
|- ( ( ( A =/= (/) /\ B =/= (/) ) /\ ( z e. A /\ w e. B ) ) -> ( ( A. x e. A A. y e. B ( ph -> x = z ) /\ A. x e. A A. x e. A A. y e. B ( ph -> y = w ) ) <-> ( A. x e. A A. y e. B ( ph -> x = z ) /\ A. x e. A A. y e. B ( ph -> y = w ) ) ) ) |
19 |
|
jcab |
|- ( ( ph -> ( x = z /\ y = w ) ) <-> ( ( ph -> x = z ) /\ ( ph -> y = w ) ) ) |
20 |
19
|
ralbii |
|- ( A. y e. B ( ph -> ( x = z /\ y = w ) ) <-> A. y e. B ( ( ph -> x = z ) /\ ( ph -> y = w ) ) ) |
21 |
|
r19.26 |
|- ( A. y e. B ( ( ph -> x = z ) /\ ( ph -> y = w ) ) <-> ( A. y e. B ( ph -> x = z ) /\ A. y e. B ( ph -> y = w ) ) ) |
22 |
20 21
|
bitri |
|- ( A. y e. B ( ph -> ( x = z /\ y = w ) ) <-> ( A. y e. B ( ph -> x = z ) /\ A. y e. B ( ph -> y = w ) ) ) |
23 |
22
|
ralbii |
|- ( A. x e. A A. y e. B ( ph -> ( x = z /\ y = w ) ) <-> A. x e. A ( A. y e. B ( ph -> x = z ) /\ A. y e. B ( ph -> y = w ) ) ) |
24 |
|
r19.26 |
|- ( A. x e. A ( A. y e. B ( ph -> x = z ) /\ A. y e. B ( ph -> y = w ) ) <-> ( A. x e. A A. y e. B ( ph -> x = z ) /\ A. x e. A A. y e. B ( ph -> y = w ) ) ) |
25 |
23 24
|
bitri |
|- ( A. x e. A A. y e. B ( ph -> ( x = z /\ y = w ) ) <-> ( A. x e. A A. y e. B ( ph -> x = z ) /\ A. x e. A A. y e. B ( ph -> y = w ) ) ) |
26 |
25
|
a1i |
|- ( ( ( A =/= (/) /\ B =/= (/) ) /\ ( z e. A /\ w e. B ) ) -> ( A. x e. A A. y e. B ( ph -> ( x = z /\ y = w ) ) <-> ( A. x e. A A. y e. B ( ph -> x = z ) /\ A. x e. A A. y e. B ( ph -> y = w ) ) ) ) |
27 |
18 26
|
bitr4d |
|- ( ( ( A =/= (/) /\ B =/= (/) ) /\ ( z e. A /\ w e. B ) ) -> ( ( A. x e. A A. y e. B ( ph -> x = z ) /\ A. x e. A A. x e. A A. y e. B ( ph -> y = w ) ) <-> A. x e. A A. y e. B ( ph -> ( x = z /\ y = w ) ) ) ) |
28 |
12 27
|
bitr2id |
|- ( ( ( A =/= (/) /\ B =/= (/) ) /\ ( z e. A /\ w e. B ) ) -> ( A. x e. A A. y e. B ( ph -> ( x = z /\ y = w ) ) <-> A. x e. A ( A. y e. B ( ph -> x = z ) /\ A. x e. A A. y e. B ( ph -> y = w ) ) ) ) |
29 |
|
r19.26 |
|- ( A. y e. B ( A. y e. B ( ph -> x = z ) /\ A. x e. A ( ph -> y = w ) ) <-> ( A. y e. B A. y e. B ( ph -> x = z ) /\ A. y e. B A. x e. A ( ph -> y = w ) ) ) |
30 |
|
nfra1 |
|- F/ y A. y e. B ( ph -> x = z ) |
31 |
30
|
r19.3rz |
|- ( B =/= (/) -> ( A. y e. B ( ph -> x = z ) <-> A. y e. B A. y e. B ( ph -> x = z ) ) ) |
32 |
31
|
ad2antlr |
|- ( ( ( A =/= (/) /\ B =/= (/) ) /\ ( z e. A /\ w e. B ) ) -> ( A. y e. B ( ph -> x = z ) <-> A. y e. B A. y e. B ( ph -> x = z ) ) ) |
33 |
32
|
bicomd |
|- ( ( ( A =/= (/) /\ B =/= (/) ) /\ ( z e. A /\ w e. B ) ) -> ( A. y e. B A. y e. B ( ph -> x = z ) <-> A. y e. B ( ph -> x = z ) ) ) |
34 |
|
ralcom |
|- ( A. y e. B A. x e. A ( ph -> y = w ) <-> A. x e. A A. y e. B ( ph -> y = w ) ) |
35 |
34
|
a1i |
|- ( ( ( A =/= (/) /\ B =/= (/) ) /\ ( z e. A /\ w e. B ) ) -> ( A. y e. B A. x e. A ( ph -> y = w ) <-> A. x e. A A. y e. B ( ph -> y = w ) ) ) |
36 |
33 35
|
anbi12d |
|- ( ( ( A =/= (/) /\ B =/= (/) ) /\ ( z e. A /\ w e. B ) ) -> ( ( A. y e. B A. y e. B ( ph -> x = z ) /\ A. y e. B A. x e. A ( ph -> y = w ) ) <-> ( A. y e. B ( ph -> x = z ) /\ A. x e. A A. y e. B ( ph -> y = w ) ) ) ) |
37 |
29 36
|
syl5bb |
|- ( ( ( A =/= (/) /\ B =/= (/) ) /\ ( z e. A /\ w e. B ) ) -> ( A. y e. B ( A. y e. B ( ph -> x = z ) /\ A. x e. A ( ph -> y = w ) ) <-> ( A. y e. B ( ph -> x = z ) /\ A. x e. A A. y e. B ( ph -> y = w ) ) ) ) |
38 |
37
|
ralbidv |
|- ( ( ( A =/= (/) /\ B =/= (/) ) /\ ( z e. A /\ w e. B ) ) -> ( A. x e. A A. y e. B ( A. y e. B ( ph -> x = z ) /\ A. x e. A ( ph -> y = w ) ) <-> A. x e. A ( A. y e. B ( ph -> x = z ) /\ A. x e. A A. y e. B ( ph -> y = w ) ) ) ) |
39 |
28 38
|
bitr4d |
|- ( ( ( A =/= (/) /\ B =/= (/) ) /\ ( z e. A /\ w e. B ) ) -> ( A. x e. A A. y e. B ( ph -> ( x = z /\ y = w ) ) <-> A. x e. A A. y e. B ( A. y e. B ( ph -> x = z ) /\ A. x e. A ( ph -> y = w ) ) ) ) |
40 |
|
r19.23v |
|- ( A. y e. B ( ph -> x = z ) <-> ( E. y e. B ph -> x = z ) ) |
41 |
|
r19.23v |
|- ( A. x e. A ( ph -> y = w ) <-> ( E. x e. A ph -> y = w ) ) |
42 |
40 41
|
anbi12i |
|- ( ( A. y e. B ( ph -> x = z ) /\ A. x e. A ( ph -> y = w ) ) <-> ( ( E. y e. B ph -> x = z ) /\ ( E. x e. A ph -> y = w ) ) ) |
43 |
42
|
2ralbii |
|- ( A. x e. A A. y e. B ( A. y e. B ( ph -> x = z ) /\ A. x e. A ( ph -> y = w ) ) <-> A. x e. A A. y e. B ( ( E. y e. B ph -> x = z ) /\ ( E. x e. A ph -> y = w ) ) ) |
44 |
43
|
a1i |
|- ( ( ( A =/= (/) /\ B =/= (/) ) /\ ( z e. A /\ w e. B ) ) -> ( A. x e. A A. y e. B ( A. y e. B ( ph -> x = z ) /\ A. x e. A ( ph -> y = w ) ) <-> A. x e. A A. y e. B ( ( E. y e. B ph -> x = z ) /\ ( E. x e. A ph -> y = w ) ) ) ) |
45 |
|
neneq |
|- ( A =/= (/) -> -. A = (/) ) |
46 |
|
neneq |
|- ( B =/= (/) -> -. B = (/) ) |
47 |
45 46
|
anim12i |
|- ( ( A =/= (/) /\ B =/= (/) ) -> ( -. A = (/) /\ -. B = (/) ) ) |
48 |
47
|
olcd |
|- ( ( A =/= (/) /\ B =/= (/) ) -> ( ( A = (/) /\ B = (/) ) \/ ( -. A = (/) /\ -. B = (/) ) ) ) |
49 |
|
dfbi3 |
|- ( ( A = (/) <-> B = (/) ) <-> ( ( A = (/) /\ B = (/) ) \/ ( -. A = (/) /\ -. B = (/) ) ) ) |
50 |
48 49
|
sylibr |
|- ( ( A =/= (/) /\ B =/= (/) ) -> ( A = (/) <-> B = (/) ) ) |
51 |
|
nfre1 |
|- F/ y E. y e. B ph |
52 |
|
nfv |
|- F/ y x = z |
53 |
51 52
|
nfim |
|- F/ y ( E. y e. B ph -> x = z ) |
54 |
|
nfre1 |
|- F/ x E. x e. A ph |
55 |
|
nfv |
|- F/ x y = w |
56 |
54 55
|
nfim |
|- F/ x ( E. x e. A ph -> y = w ) |
57 |
53 56
|
raaan2 |
|- ( ( A = (/) <-> B = (/) ) -> ( A. x e. A A. y e. B ( ( E. y e. B ph -> x = z ) /\ ( E. x e. A ph -> y = w ) ) <-> ( A. x e. A ( E. y e. B ph -> x = z ) /\ A. y e. B ( E. x e. A ph -> y = w ) ) ) ) |
58 |
50 57
|
syl |
|- ( ( A =/= (/) /\ B =/= (/) ) -> ( A. x e. A A. y e. B ( ( E. y e. B ph -> x = z ) /\ ( E. x e. A ph -> y = w ) ) <-> ( A. x e. A ( E. y e. B ph -> x = z ) /\ A. y e. B ( E. x e. A ph -> y = w ) ) ) ) |
59 |
58
|
adantr |
|- ( ( ( A =/= (/) /\ B =/= (/) ) /\ ( z e. A /\ w e. B ) ) -> ( A. x e. A A. y e. B ( ( E. y e. B ph -> x = z ) /\ ( E. x e. A ph -> y = w ) ) <-> ( A. x e. A ( E. y e. B ph -> x = z ) /\ A. y e. B ( E. x e. A ph -> y = w ) ) ) ) |
60 |
39 44 59
|
3bitrd |
|- ( ( ( A =/= (/) /\ B =/= (/) ) /\ ( z e. A /\ w e. B ) ) -> ( A. x e. A A. y e. B ( ph -> ( x = z /\ y = w ) ) <-> ( A. x e. A ( E. y e. B ph -> x = z ) /\ A. y e. B ( E. x e. A ph -> y = w ) ) ) ) |
61 |
60
|
2rexbidva |
|- ( ( A =/= (/) /\ B =/= (/) ) -> ( E. z e. A E. w e. B A. x e. A A. y e. B ( ph -> ( x = z /\ y = w ) ) <-> E. z e. A E. w e. B ( A. x e. A ( E. y e. B ph -> x = z ) /\ A. y e. B ( E. x e. A ph -> y = w ) ) ) ) |
62 |
|
reeanv |
|- ( E. z e. A E. w e. B ( A. x e. A ( E. y e. B ph -> x = z ) /\ A. y e. B ( E. x e. A ph -> y = w ) ) <-> ( E. z e. A A. x e. A ( E. y e. B ph -> x = z ) /\ E. w e. B A. y e. B ( E. x e. A ph -> y = w ) ) ) |
63 |
61 62
|
bitr2di |
|- ( ( A =/= (/) /\ B =/= (/) ) -> ( ( E. z e. A A. x e. A ( E. y e. B ph -> x = z ) /\ E. w e. B A. y e. B ( E. x e. A ph -> y = w ) ) <-> E. z e. A E. w e. B A. x e. A A. y e. B ( ph -> ( x = z /\ y = w ) ) ) ) |
64 |
11 63
|
anbi12d |
|- ( ( A =/= (/) /\ B =/= (/) ) -> ( ( ( E. x e. A E. y e. B ph /\ E. y e. B E. x e. A ph ) /\ ( E. z e. A A. x e. A ( E. y e. B ph -> x = z ) /\ E. w e. B A. y e. B ( E. x e. A ph -> y = w ) ) ) <-> ( E. x e. A E. y e. B ph /\ E. z e. A E. w e. B A. x e. A A. y e. B ( ph -> ( x = z /\ y = w ) ) ) ) ) |
65 |
4 6 64
|
3bitrd |
|- ( ( A =/= (/) /\ B =/= (/) ) -> ( ( E! x e. A E. y e. B ph /\ E! y e. B E. x e. A ph ) <-> ( E. x e. A E. y e. B ph /\ E. z e. A E. w e. B A. x e. A A. y e. B ( ph -> ( x = z /\ y = w ) ) ) ) ) |