Metamath Proof Explorer

Theorem euoreqb

Description: There is a set which is equal to one of two other sets iff the other sets are equal. (Contributed by AV, 24-Jan-2023)

Ref Expression
Assertion euoreqb 
|- ( ( A e. V /\ B e. V ) -> ( E! x e. V ( x = A \/ x = B ) <-> A = B ) )

Proof

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 biimtrid 
 |-  ( ( 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 ) )