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 e. _V
	opthreg.2	|- B e. _V
	opthreg.3	|- C e. _V
	opthreg.4	|- D e. _V
Assertion	opthreg	|- ( { A , { A , B } } = { C , { C , D } } <-> ( A = C /\ B = D ) )

Proof

Step	Hyp	Ref	Expression
1		opthreg.1	|- A e. _V
2		opthreg.2	|- B e. _V
3		opthreg.3	|- C e. _V
4		opthreg.4	|- D e. _V
5	1	prid1	|- A e. { A , B }
6	3	prid1	|- C e. { C , D }
7		prex	|- { A , B } e. _V
8	7	preleq	|- ( ( ( A e. { A , B } /\ C e. { 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 ) )