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	⊢ 𝐴 ∈ V
	opthreg.2	⊢ 𝐵 ∈ V
	opthreg.3	⊢ 𝐶 ∈ V
	opthreg.4	⊢ 𝐷 ∈ V
Assertion	opthreg	⊢ ( { 𝐴 , { 𝐴 , 𝐵 } } = { 𝐶 , { 𝐶 , 𝐷 } } ↔ ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) )

Proof

Step	Hyp	Ref	Expression
1		opthreg.1	⊢ 𝐴 ∈ V
2		opthreg.2	⊢ 𝐵 ∈ V
3		opthreg.3	⊢ 𝐶 ∈ V
4		opthreg.4	⊢ 𝐷 ∈ V
5	1	prid1	⊢ 𝐴 ∈ { 𝐴 , 𝐵 }
6	3	prid1	⊢ 𝐶 ∈ { 𝐶 , 𝐷 }
7		prex	⊢ { 𝐴 , 𝐵 } ∈ V
8	7	preleq	⊢ ( ( ( 𝐴 ∈ { 𝐴 , 𝐵 } ∧ 𝐶 ∈ { 𝐶 , 𝐷 } ) ∧ { 𝐴 , { 𝐴 , 𝐵 } } = { 𝐶 , { 𝐶 , 𝐷 } } ) → ( 𝐴 = 𝐶 ∧ { 𝐴 , 𝐵 } = { 𝐶 , 𝐷 } ) )
9	5 6 8	mpanl12	⊢ ( { 𝐴 , { 𝐴 , 𝐵 } } = { 𝐶 , { 𝐶 , 𝐷 } } → ( 𝐴 = 𝐶 ∧ { 𝐴 , 𝐵 } = { 𝐶 , 𝐷 } ) )
10		preq1	⊢ ( 𝐴 = 𝐶 → { 𝐴 , 𝐵 } = { 𝐶 , 𝐵 } )
11	10	eqeq1d	⊢ ( 𝐴 = 𝐶 → ( { 𝐴 , 𝐵 } = { 𝐶 , 𝐷 } ↔ { 𝐶 , 𝐵 } = { 𝐶 , 𝐷 } ) )
12	2 4	preqr2	⊢ ( { 𝐶 , 𝐵 } = { 𝐶 , 𝐷 } → 𝐵 = 𝐷 )
13	11 12	syl6bi	⊢ ( 𝐴 = 𝐶 → ( { 𝐴 , 𝐵 } = { 𝐶 , 𝐷 } → 𝐵 = 𝐷 ) )
14	13	imdistani	⊢ ( ( 𝐴 = 𝐶 ∧ { 𝐴 , 𝐵 } = { 𝐶 , 𝐷 } ) → ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) )
15	9 14	syl	⊢ ( { 𝐴 , { 𝐴 , 𝐵 } } = { 𝐶 , { 𝐶 , 𝐷 } } → ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) )
16		preq1	⊢ ( 𝐴 = 𝐶 → { 𝐴 , { 𝐴 , 𝐵 } } = { 𝐶 , { 𝐴 , 𝐵 } } )
17	16	adantr	⊢ ( ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) → { 𝐴 , { 𝐴 , 𝐵 } } = { 𝐶 , { 𝐴 , 𝐵 } } )
18		preq12	⊢ ( ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) → { 𝐴 , 𝐵 } = { 𝐶 , 𝐷 } )
19	18	preq2d	⊢ ( ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) → { 𝐶 , { 𝐴 , 𝐵 } } = { 𝐶 , { 𝐶 , 𝐷 } } )
20	17 19	eqtrd	⊢ ( ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) → { 𝐴 , { 𝐴 , 𝐵 } } = { 𝐶 , { 𝐶 , 𝐷 } } )
21	15 20	impbii	⊢ ( { 𝐴 , { 𝐴 , 𝐵 } } = { 𝐶 , { 𝐶 , 𝐷 } } ↔ ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) )