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