Step |
Hyp |
Ref |
Expression |
1 |
|
eqeq1 |
|- ( x = y -> ( x = A <-> y = A ) ) |
2 |
|
eqeq1 |
|- ( x = y -> ( x = B <-> y = B ) ) |
3 |
1 2
|
orbi12d |
|- ( x = y -> ( ( x = A \/ x = B ) <-> ( y = A \/ y = B ) ) ) |
4 |
3
|
reu8 |
|- ( E! x e. V ( x = A \/ x = B ) <-> E. x e. V ( ( x = A \/ x = B ) /\ A. y e. V ( ( y = A \/ y = B ) -> x = y ) ) ) |
5 |
|
simprlr |
|- ( ( x = A /\ ( ( A e. V /\ B e. V ) /\ x e. V ) ) -> B e. V ) |
6 |
|
eqeq1 |
|- ( y = B -> ( y = A <-> B = A ) ) |
7 |
|
eqeq1 |
|- ( y = B -> ( y = B <-> B = B ) ) |
8 |
6 7
|
orbi12d |
|- ( y = B -> ( ( y = A \/ y = B ) <-> ( B = A \/ B = B ) ) ) |
9 |
|
eqeq2 |
|- ( y = B -> ( x = y <-> x = B ) ) |
10 |
8 9
|
imbi12d |
|- ( y = B -> ( ( ( y = A \/ y = B ) -> x = y ) <-> ( ( B = A \/ B = B ) -> x = B ) ) ) |
11 |
10
|
rspcv |
|- ( B e. V -> ( A. y e. V ( ( y = A \/ y = B ) -> x = y ) -> ( ( B = A \/ B = B ) -> x = B ) ) ) |
12 |
5 11
|
syl |
|- ( ( x = A /\ ( ( A e. V /\ B e. V ) /\ x e. V ) ) -> ( A. y e. V ( ( y = A \/ y = B ) -> x = y ) -> ( ( B = A \/ B = B ) -> x = B ) ) ) |
13 |
|
ioran |
|- ( -. ( B = A \/ B = B ) <-> ( -. B = A /\ -. B = B ) ) |
14 |
|
eqid |
|- B = B |
15 |
14
|
pm2.24i |
|- ( -. B = B -> ( ( x = A /\ ( ( A e. V /\ B e. V ) /\ x e. V ) ) -> A = B ) ) |
16 |
13 15
|
simplbiim |
|- ( -. ( B = A \/ B = B ) -> ( ( x = A /\ ( ( A e. V /\ B e. V ) /\ x e. V ) ) -> A = B ) ) |
17 |
|
eqtr2 |
|- ( ( x = A /\ x = B ) -> A = B ) |
18 |
17
|
ancoms |
|- ( ( x = B /\ x = A ) -> A = B ) |
19 |
18
|
a1d |
|- ( ( x = B /\ x = A ) -> ( ( ( A e. V /\ B e. V ) /\ x e. V ) -> A = B ) ) |
20 |
19
|
expimpd |
|- ( x = B -> ( ( x = A /\ ( ( A e. V /\ B e. V ) /\ x e. V ) ) -> A = B ) ) |
21 |
16 20
|
ja |
|- ( ( ( B = A \/ B = B ) -> x = B ) -> ( ( x = A /\ ( ( A e. V /\ B e. V ) /\ x e. V ) ) -> A = B ) ) |
22 |
21
|
com12 |
|- ( ( x = A /\ ( ( A e. V /\ B e. V ) /\ x e. V ) ) -> ( ( ( B = A \/ B = B ) -> x = B ) -> A = B ) ) |
23 |
12 22
|
syld |
|- ( ( x = A /\ ( ( A e. V /\ B e. V ) /\ x e. V ) ) -> ( A. y e. V ( ( y = A \/ y = B ) -> x = y ) -> A = B ) ) |
24 |
23
|
ex |
|- ( x = A -> ( ( ( A e. V /\ B e. V ) /\ x e. V ) -> ( A. y e. V ( ( y = A \/ y = B ) -> x = y ) -> A = B ) ) ) |
25 |
|
simprll |
|- ( ( x = B /\ ( ( A e. V /\ B e. V ) /\ x e. V ) ) -> A e. V ) |
26 |
|
eqeq1 |
|- ( y = A -> ( y = A <-> A = A ) ) |
27 |
|
eqeq1 |
|- ( y = A -> ( y = B <-> A = B ) ) |
28 |
26 27
|
orbi12d |
|- ( y = A -> ( ( y = A \/ y = B ) <-> ( A = A \/ A = B ) ) ) |
29 |
|
eqeq2 |
|- ( y = A -> ( x = y <-> x = A ) ) |
30 |
28 29
|
imbi12d |
|- ( y = A -> ( ( ( y = A \/ y = B ) -> x = y ) <-> ( ( A = A \/ A = B ) -> x = A ) ) ) |
31 |
30
|
rspcv |
|- ( A e. V -> ( A. y e. V ( ( y = A \/ y = B ) -> x = y ) -> ( ( A = A \/ A = B ) -> x = A ) ) ) |
32 |
25 31
|
syl |
|- ( ( x = B /\ ( ( A e. V /\ B e. V ) /\ x e. V ) ) -> ( A. y e. V ( ( y = A \/ y = B ) -> x = y ) -> ( ( A = A \/ A = B ) -> x = A ) ) ) |
33 |
|
ioran |
|- ( -. ( A = A \/ A = B ) <-> ( -. A = A /\ -. A = B ) ) |
34 |
|
eqid |
|- A = A |
35 |
34
|
pm2.24i |
|- ( -. A = A -> ( ( x = B /\ ( ( A e. V /\ B e. V ) /\ x e. V ) ) -> A = B ) ) |
36 |
35
|
adantr |
|- ( ( -. A = A /\ -. A = B ) -> ( ( x = B /\ ( ( A e. V /\ B e. V ) /\ x e. V ) ) -> A = B ) ) |
37 |
33 36
|
sylbi |
|- ( -. ( A = A \/ A = B ) -> ( ( x = B /\ ( ( A e. V /\ B e. V ) /\ x e. V ) ) -> A = B ) ) |
38 |
17
|
a1d |
|- ( ( x = A /\ x = B ) -> ( ( ( A e. V /\ B e. V ) /\ x e. V ) -> A = B ) ) |
39 |
38
|
expimpd |
|- ( x = A -> ( ( x = B /\ ( ( A e. V /\ B e. V ) /\ x e. V ) ) -> A = B ) ) |
40 |
37 39
|
ja |
|- ( ( ( A = A \/ A = B ) -> x = A ) -> ( ( x = B /\ ( ( A e. V /\ B e. V ) /\ x e. V ) ) -> A = B ) ) |
41 |
40
|
com12 |
|- ( ( x = B /\ ( ( A e. V /\ B e. V ) /\ x e. V ) ) -> ( ( ( A = A \/ A = B ) -> x = A ) -> A = B ) ) |
42 |
32 41
|
syld |
|- ( ( x = B /\ ( ( A e. V /\ B e. V ) /\ x e. V ) ) -> ( A. y e. V ( ( y = A \/ y = B ) -> x = y ) -> A = B ) ) |
43 |
42
|
ex |
|- ( x = B -> ( ( ( A e. V /\ B e. V ) /\ x e. V ) -> ( A. y e. V ( ( y = A \/ y = B ) -> x = y ) -> A = B ) ) ) |
44 |
24 43
|
jaoi |
|- ( ( x = A \/ x = B ) -> ( ( ( A e. V /\ B e. V ) /\ x e. V ) -> ( A. y e. V ( ( y = A \/ y = B ) -> x = y ) -> A = B ) ) ) |
45 |
44
|
com12 |
|- ( ( ( A e. V /\ B e. V ) /\ x e. V ) -> ( ( x = A \/ x = B ) -> ( A. y e. V ( ( y = A \/ y = B ) -> x = y ) -> A = B ) ) ) |
46 |
45
|
impd |
|- ( ( ( A e. V /\ B e. V ) /\ x e. V ) -> ( ( ( x = A \/ x = B ) /\ A. y e. V ( ( y = A \/ y = B ) -> x = y ) ) -> A = B ) ) |
47 |
46
|
rexlimdva |
|- ( ( A e. V /\ B e. V ) -> ( E. x e. V ( ( x = A \/ x = B ) /\ A. y e. V ( ( y = A \/ y = B ) -> x = y ) ) -> A = B ) ) |
48 |
4 47
|
syl5bi |
|- ( ( A e. V /\ B e. V ) -> ( E! x e. V ( x = A \/ x = B ) -> A = B ) ) |
49 |
|
reueq |
|- ( B e. V <-> E! x e. V x = B ) |
50 |
49
|
biimpi |
|- ( B e. V -> E! x e. V x = B ) |
51 |
50
|
adantl |
|- ( ( A e. V /\ B e. V ) -> E! x e. V x = B ) |
52 |
51
|
adantr |
|- ( ( ( A e. V /\ B e. V ) /\ A = B ) -> E! x e. V x = B ) |
53 |
|
eqeq2 |
|- ( A = B -> ( x = A <-> x = B ) ) |
54 |
53
|
adantl |
|- ( ( ( A e. V /\ B e. V ) /\ A = B ) -> ( x = A <-> x = B ) ) |
55 |
54
|
orbi1d |
|- ( ( ( A e. V /\ B e. V ) /\ A = B ) -> ( ( x = A \/ x = B ) <-> ( x = B \/ x = B ) ) ) |
56 |
|
oridm |
|- ( ( x = B \/ x = B ) <-> x = B ) |
57 |
55 56
|
bitrdi |
|- ( ( ( A e. V /\ B e. V ) /\ A = B ) -> ( ( x = A \/ x = B ) <-> x = B ) ) |
58 |
57
|
reubidv |
|- ( ( ( A e. V /\ B e. V ) /\ A = B ) -> ( E! x e. V ( x = A \/ x = B ) <-> E! x e. V x = B ) ) |
59 |
52 58
|
mpbird |
|- ( ( ( A e. V /\ B e. V ) /\ A = B ) -> E! x e. V ( x = A \/ x = B ) ) |
60 |
59
|
ex |
|- ( ( A e. V /\ B e. V ) -> ( A = B -> E! x e. V ( x = A \/ x = B ) ) ) |
61 |
48 60
|
impbid |
|- ( ( A e. V /\ B e. V ) -> ( E! x e. V ( x = A \/ x = B ) <-> A = B ) ) |