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 ⊢ A B = C D ↔ A = C ∧ B = D

Proof

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