Theorem opthreg 4622

Description: Theorem for alternate representation of ordered pairs, requiring the Axiom of Set Induction ax-setind 4603 (via the preleq 4621 step). See df-op 3652 for a description of other ordered pair representations. Exercise 34 of [Enderton] p. 207. (Contributed by NM, 16-Oct-1996.)

Hypotheses

Ref	Expression
preleq.1	⊢ 𝐴 ∈ V
preleq.2	⊢ 𝐵 ∈ V
preleq.3	⊢ 𝐶 ∈ V
preleq.4	⊢ 𝐷 ∈ V

Assertion

Ref	Expression
opthreg	⊢ ({𝐴, {𝐴, 𝐵}} = {𝐶, {𝐶, 𝐷}} ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷))

Proof of Theorem opthreg

Step	Hyp	Ref	Expression
1		preleq.1	. . . . 5 ⊢ 𝐴 ∈ V
2	1	prid1 3749	. . . 4 ⊢ 𝐴 ∈ {𝐴, 𝐵}
3		preleq.3	. . . . 5 ⊢ 𝐶 ∈ V
4	3	prid1 3749	. . . 4 ⊢ 𝐶 ∈ {𝐶, 𝐷}
5		preleq.2	. . . . . 6 ⊢ 𝐵 ∈ V
6		prexg 4271	. . . . . 6 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → {𝐴, 𝐵} ∈ V)
7	1, 5, 6	mp2an 426	. . . . 5 ⊢ {𝐴, 𝐵} ∈ V
8		preleq.4	. . . . . 6 ⊢ 𝐷 ∈ V
9		prexg 4271	. . . . . 6 ⊢ ((𝐶 ∈ V ∧ 𝐷 ∈ V) → {𝐶, 𝐷} ∈ V)
10	3, 8, 9	mp2an 426	. . . . 5 ⊢ {𝐶, 𝐷} ∈ V
11	1, 7, 3, 10	preleq 4621	. . . 4 ⊢ (((𝐴 ∈ {𝐴, 𝐵} ∧ 𝐶 ∈ {𝐶, 𝐷}) ∧ {𝐴, {𝐴, 𝐵}} = {𝐶, {𝐶, 𝐷}}) → (𝐴 = 𝐶 ∧ {𝐴, 𝐵} = {𝐶, 𝐷}))
12	2, 4, 11	mpanl12 436	. . 3 ⊢ ({𝐴, {𝐴, 𝐵}} = {𝐶, {𝐶, 𝐷}} → (𝐴 = 𝐶 ∧ {𝐴, 𝐵} = {𝐶, 𝐷}))
13		preq1 3720	. . . . . 6 ⊢ (𝐴 = 𝐶 → {𝐴, 𝐵} = {𝐶, 𝐵})
14	13	eqeq1d 2216	. . . . 5 ⊢ (𝐴 = 𝐶 → ({𝐴, 𝐵} = {𝐶, 𝐷} ↔ {𝐶, 𝐵} = {𝐶, 𝐷}))
15	5, 8	preqr2 3823	. . . . 5 ⊢ ({𝐶, 𝐵} = {𝐶, 𝐷} → 𝐵 = 𝐷)
16	14, 15	biimtrdi 163	. . . 4 ⊢ (𝐴 = 𝐶 → ({𝐴, 𝐵} = {𝐶, 𝐷} → 𝐵 = 𝐷))
17	16	imdistani 445	. . 3 ⊢ ((𝐴 = 𝐶 ∧ {𝐴, 𝐵} = {𝐶, 𝐷}) → (𝐴 = 𝐶 ∧ 𝐵 = 𝐷))
18	12, 17	syl 14	. 2 ⊢ ({𝐴, {𝐴, 𝐵}} = {𝐶, {𝐶, 𝐷}} → (𝐴 = 𝐶 ∧ 𝐵 = 𝐷))
19		preq1 3720	. . . 4 ⊢ (𝐴 = 𝐶 → {𝐴, {𝐴, 𝐵}} = {𝐶, {𝐴, 𝐵}})
20	19	adantr 276	. . 3 ⊢ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) → {𝐴, {𝐴, 𝐵}} = {𝐶, {𝐴, 𝐵}})
21		preq12 3722	. . . 4 ⊢ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) → {𝐴, 𝐵} = {𝐶, 𝐷})
22	21	preq2d 3727	. . 3 ⊢ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) → {𝐶, {𝐴, 𝐵}} = {𝐶, {𝐶, 𝐷}})
23	20, 22	eqtrd 2240	. 2 ⊢ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) → {𝐴, {𝐴, 𝐵}} = {𝐶, {𝐶, 𝐷}})
24	18, 23	impbii 126	1 ⊢ ({𝐴, {𝐴, 𝐵}} = {𝐶, {𝐶, 𝐷}} ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷))

Syntax hints:   ∧ wa 104   ↔ wb 105   = wceq 1373   ∈ wcel 2178  Vcvv 2776  {cpr 3644

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 615  ax-in2 616  ax-io 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-14 2181  ax-ext 2189  ax-sep 4178  ax-pr 4269  ax-setind 4603

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2194  df-cleq 2200  df-clel 2203  df-nfc 2339  df-ral 2491  df-v 2778  df-dif 3176  df-un 3178  df-sn 3649  df-pr 3650

This theorem is referenced by: (None)