Metamath Proof Explorer

Theorem snopeqop

Description: Equivalence for an ordered pair equal to a singleton of an ordered pair. (Contributed by AV, 18-Sep-2020) (Revised by AV, 15-Jul-2022) (Avoid depending on this detail.)

Ref Expression
Hypotheses snopeqop.a ⊢A∈V
snopeqop.b ⊢B∈V
Assertion snopeqop ⊢AB=CD↔A=B∧C=D∧C=A

Proof

Step Hyp Ref Expression
1 snopeqop.a ⊢A∈V
2 snopeqop.b ⊢B∈V
3 eqcom ⊢AB=CD↔CD=AB
4 opeqsng ⊢C∈V∧D∈V→CD=AB↔C=D∧AB=C
5 4 ancoms ⊢D∈V∧C∈V→CD=AB↔C=D∧AB=C
6 3 5 bitrid ⊢D∈V∧C∈V→AB=CD↔C=D∧AB=C
7 1 2 opeqsn ⊢AB=C↔A=B∧C=A
8 7 a1i ⊢D∈V∧C∈V→AB=C↔A=B∧C=A
9 8 anbi2d ⊢D∈V∧C∈V→C=D∧AB=C↔C=D∧A=B∧C=A
10 3anan12 ⊢A=B∧C=D∧C=A↔C=D∧A=B∧C=A
11 10 bicomi ⊢C=D∧A=B∧C=A↔A=B∧C=D∧C=A
12 11 a1i ⊢D∈V∧C∈V→C=D∧A=B∧C=A↔A=B∧C=D∧C=A
13 6 9 12 3bitrd ⊢D∈V∧C∈V→AB=CD↔A=B∧C=D∧C=A
14 opprc2 ⊢¬D∈V→CD=∅
15 14 eqeq2d ⊢¬D∈V→AB=CD↔AB=∅
16 opex ⊢AB∈V
17 16 snnz ⊢AB≠∅
18 eqneqall ⊢AB=∅→AB≠∅→A=B∧C=D∧C=A
19 17 18 mpi ⊢AB=∅→A=B∧C=D∧C=A
20 15 19 biimtrdi ⊢¬D∈V→AB=CD→A=B∧C=D∧C=A
21 20 adantr ⊢¬D∈V∧C∈V→AB=CD→A=B∧C=D∧C=A
22 eleq1 ⊢D=C→D∈V↔C∈V
23 22 notbid ⊢D=C→¬D∈V↔¬C∈V
24 23 eqcoms ⊢C=D→¬D∈V↔¬C∈V
25 pm2.21 ⊢¬C∈V→C∈V→AB=CD
26 24 25 biimtrdi ⊢C=D→¬D∈V→C∈V→AB=CD
27 26 impd ⊢C=D→¬D∈V∧C∈V→AB=CD
28 27 3ad2ant2 ⊢A=B∧C=D∧C=A→¬D∈V∧C∈V→AB=CD
29 28 com12 ⊢¬D∈V∧C∈V→A=B∧C=D∧C=A→AB=CD
30 21 29 impbid ⊢¬D∈V∧C∈V→AB=CD↔A=B∧C=D∧C=A
31 13 30 pm2.61ian ⊢C∈V→AB=CD↔A=B∧C=D∧C=A
32 opprc1 ⊢¬C∈V→CD=∅
33 32 eqeq2d ⊢¬C∈V→AB=CD↔AB=∅
34 33 19 biimtrdi ⊢¬C∈V→AB=CD→A=B∧C=D∧C=A
35 eleq1 ⊢C=A→C∈V↔A∈V
36 35 notbid ⊢C=A→¬C∈V↔¬A∈V
37 snex ⊢A∈V
38 37 pm2.24i ⊢¬A∈V→AB=CD
39 36 38 biimtrdi ⊢C=A→¬C∈V→AB=CD
40 39 3ad2ant3 ⊢A=B∧C=D∧C=A→¬C∈V→AB=CD
41 40 com12 ⊢¬C∈V→A=B∧C=D∧C=A→AB=CD
42 34 41 impbid ⊢¬C∈V→AB=CD↔A=B∧C=D∧C=A
43 31 42 pm2.61i ⊢AB=CD↔A=B∧C=D∧C=A