Metamath Proof Explorer

Theorem opthreg

Description: Theorem for alternate representation of ordered pairs, requiring the Axiom of Regularity ax-reg (via the preleq step). See df-op for a description of other ordered pair representations. Exercise 34 of Enderton p. 207. (Contributed by NM, 16-Oct-1996) (Proof shortened by AV, 15-Jun-2022)

Ref Expression
Hypotheses opthreg.1 ⊢ A ∈ V
opthreg.2 ⊢ B ∈ V
opthreg.3 ⊢ C ∈ V
opthreg.4 ⊢ D ∈ V
Assertion opthreg ⊢ A A B = C C D ↔ A = C ∧ B = D

Proof

Step Hyp Ref Expression
1 opthreg.1 ⊢ A ∈ V
2 opthreg.2 ⊢ B ∈ V
3 opthreg.3 ⊢ C ∈ V
4 opthreg.4 ⊢ D ∈ V
5 1 prid1 ⊢ A ∈ A B
6 3 prid1 ⊢ C ∈ C D
7 prex ⊢ A B ∈ V
8 7 preleq ⊢ A ∈ A B ∧ C ∈ C D ∧ A A B = C C D → A = C ∧ A B = C D
9 5 6 8 mpanl12 ⊢ A A B = C C D → A = C ∧ A B = C D
10 preq1 ⊢ A = C → A B = C B
11 10 eqeq1d ⊢ A = C → A B = C D ↔ C B = C D
12 2 4 preqr2 ⊢ C B = C D → B = D
13 11 12 biimtrdi ⊢ A = C → A B = C D → B = D
14 13 imdistani ⊢ A = C ∧ A B = C D → A = C ∧ B = D
15 9 14 syl ⊢ A A B = C C D → A = C ∧ B = D
16 preq1 ⊢ A = C → A A B = C A B
17 16 adantr ⊢ A = C ∧ B = D → A A B = C A B
18 preq12 ⊢ A = C ∧ B = D → A B = C D
19 18 preq2d ⊢ A = C ∧ B = D → C A B = C C D
20 17 19 eqtrd ⊢ A = C ∧ B = D → A A B = C C D
21 15 20 impbii ⊢ A A B = C C D ↔ A = C ∧ B = D