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∈V∧B∈V→∃!x∈Vx=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 ⊢∃!x∈Vx=A∨x=B↔∃x∈Vx=A∨x=B∧∀y∈Vy=A∨y=B→x=y
5 simprlr ⊢x=A∧A∈V∧B∈V∧x∈V→B∈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∈V→∀y∈Vy=A∨y=B→x=y→B=A∨B=B→x=B
12 5 11 syl ⊢x=A∧A∈V∧B∈V∧x∈V→∀y∈Vy=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∈V∧B∈V∧x∈V→A=B
16 13 15 simplbiim ⊢¬B=A∨B=B→x=A∧A∈V∧B∈V∧x∈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∈V∧B∈V∧x∈V→A=B
20 19 expimpd ⊢x=B→x=A∧A∈V∧B∈V∧x∈V→A=B
21 16 20 ja ⊢B=A∨B=B→x=B→x=A∧A∈V∧B∈V∧x∈V→A=B
22 21 com12 ⊢x=A∧A∈V∧B∈V∧x∈V→B=A∨B=B→x=B→A=B
23 12 22 syld ⊢x=A∧A∈V∧B∈V∧x∈V→∀y∈Vy=A∨y=B→x=y→A=B
24 23 ex ⊢x=A→A∈V∧B∈V∧x∈V→∀y∈Vy=A∨y=B→x=y→A=B
25 simprll ⊢x=B∧A∈V∧B∈V∧x∈V→A∈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∈V→∀y∈Vy=A∨y=B→x=y→A=A∨A=B→x=A
32 25 31 syl ⊢x=B∧A∈V∧B∈V∧x∈V→∀y∈Vy=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∈V∧B∈V∧x∈V→A=B
36 35 adantr ⊢¬A=A∧¬A=B→x=B∧A∈V∧B∈V∧x∈V→A=B
37 33 36 sylbi ⊢¬A=A∨A=B→x=B∧A∈V∧B∈V∧x∈V→A=B
38 17 a1d ⊢x=A∧x=B→A∈V∧B∈V∧x∈V→A=B
39 38 expimpd ⊢x=A→x=B∧A∈V∧B∈V∧x∈V→A=B
40 37 39 ja ⊢A=A∨A=B→x=A→x=B∧A∈V∧B∈V∧x∈V→A=B
41 40 com12 ⊢x=B∧A∈V∧B∈V∧x∈V→A=A∨A=B→x=A→A=B
42 32 41 syld ⊢x=B∧A∈V∧B∈V∧x∈V→∀y∈Vy=A∨y=B→x=y→A=B
43 42 ex ⊢x=B→A∈V∧B∈V∧x∈V→∀y∈Vy=A∨y=B→x=y→A=B
44 24 43 jaoi ⊢x=A∨x=B→A∈V∧B∈V∧x∈V→∀y∈Vy=A∨y=B→x=y→A=B
45 44 com12 ⊢A∈V∧B∈V∧x∈V→x=A∨x=B→∀y∈Vy=A∨y=B→x=y→A=B
46 45 impd ⊢A∈V∧B∈V∧x∈V→x=A∨x=B∧∀y∈Vy=A∨y=B→x=y→A=B
47 46 rexlimdva ⊢A∈V∧B∈V→∃x∈Vx=A∨x=B∧∀y∈Vy=A∨y=B→x=y→A=B
48 4 47 biimtrid ⊢A∈V∧B∈V→∃!x∈Vx=A∨x=B→A=B
49 reueq ⊢B∈V↔∃!x∈Vx=B
50 49 biimpi ⊢B∈V→∃!x∈Vx=B
51 50 adantl ⊢A∈V∧B∈V→∃!x∈Vx=B
52 51 adantr ⊢A∈V∧B∈V∧A=B→∃!x∈Vx=B
53 eqeq2 ⊢A=B→x=A↔x=B
54 53 adantl ⊢A∈V∧B∈V∧A=B→x=A↔x=B
55 54 orbi1d ⊢A∈V∧B∈V∧A=B→x=A∨x=B↔x=B∨x=B
56 oridm ⊢x=B∨x=B↔x=B
57 55 56 bitrdi ⊢A∈V∧B∈V∧A=B→x=A∨x=B↔x=B
58 57 reubidv ⊢A∈V∧B∈V∧A=B→∃!x∈Vx=A∨x=B↔∃!x∈Vx=B
59 52 58 mpbird ⊢A∈V∧B∈V∧A=B→∃!x∈Vx=A∨x=B
60 59 ex ⊢A∈V∧B∈V→A=B→∃!x∈Vx=A∨x=B
61 48 60 impbid ⊢A∈V∧B∈V→∃!x∈Vx=A∨x=B↔A=B