Metamath Proof Explorer

Theorem altopthsn

Description: Two alternate ordered pairs are equal iff the singletons of their respective elements are equal. Note that this holds regardless of sethood of any of the elements. (Contributed by Scott Fenton, 16-Apr-2012)

Ref Expression
Assertion altopthsn ⊢AB=CD↔A=C∧B=D

Proof

Step Hyp Ref Expression
1 df-altop ⊢AB=AAB
2 df-altop ⊢CD=CCD
3 1 2 eqeq12i ⊢AB=CD↔AAB=CCD
4 snex ⊢A∈V
5 prex ⊢AB∈V
6 snex ⊢C∈V
7 prex ⊢CD∈V
8 4 5 6 7 preq12b ⊢AAB=CCD↔A=C∧AB=CD∨A=CD∧AB=C
9 simpl ⊢A=C∧AB=CD→A=C
10 snsspr1 ⊢A⊆AB
11 sseq2 ⊢AB=C→A⊆AB↔A⊆C
12 10 11 mpbii ⊢AB=C→A⊆C
13 12 adantl ⊢A=CD∧AB=C→A⊆C
14 snsspr1 ⊢C⊆CD
15 sseq2 ⊢A=CD→C⊆A↔C⊆CD
16 14 15 mpbiri ⊢A=CD→C⊆A
17 16 adantr ⊢A=CD∧AB=C→C⊆A
18 13 17 eqssd ⊢A=CD∧AB=C→A=C
19 9 18 jaoi ⊢A=C∧AB=CD∨A=CD∧AB=C→A=C
20 8 19 sylbi ⊢AAB=CCD→A=C
21 uneq1 ⊢A=C→A∪B=C∪B
22 df-pr ⊢AB=A∪B
23 df-pr ⊢CB=C∪B
24 21 22 23 3eqtr4g ⊢A=C→AB=CB
25 24 preq2d ⊢A=C→AAB=ACB
26 preq1 ⊢A=C→ACB=CCB
27 25 26 eqtrd ⊢A=C→AAB=CCB
28 27 eqeq1d ⊢A=C→AAB=CCD↔CCB=CCD
29 28 biimpd ⊢A=C→AAB=CCD→CCB=CCD
30 prex ⊢CB∈V
31 30 7 preqr2 ⊢CCB=CCD→CB=CD
32 snex ⊢B∈V
33 snex ⊢D∈V
34 32 33 preqr2 ⊢CB=CD→B=D
35 31 34 syl ⊢CCB=CCD→B=D
36 29 35 syl6com ⊢AAB=CCD→A=C→B=D
37 20 36 jcai ⊢AAB=CCD→A=C∧B=D
38 preq2 ⊢B=D→CB=CD
39 38 preq2d ⊢B=D→CCB=CCD
40 27 39 sylan9eq ⊢A=C∧B=D→AAB=CCD
41 37 40 impbii ⊢AAB=CCD↔A=C∧B=D
42 3 41 bitri ⊢AB=CD↔A=C∧B=D