Theorem opth2 2789

Description: Equality of the second members of equal ordered pairs. Because of our particular ordered pair definition, equality holds whether or not the first members are sets.

Hypotheses

Ref	Expression
opth2.1	⊢ B ∈ V
opth2.2	⊢ D ∈ V

Assertion

Ref	Expression
opth2	⊢ (⟨A, B⟩ = ⟨C, D⟩ → B = D)

Proof of Theorem opth2

Step	Hyp	Ref	Expression
1		opeq1 2478	. . . . 5 ⊢ (x = A → ⟨x, B⟩ = ⟨A, B⟩)
2	1	eqeq1d 1475	. . . 4 ⊢ (x = A → (⟨x, B⟩ = ⟨C, D⟩ ↔ ⟨A, B⟩ = ⟨C, D⟩))
3	2	imbi1d 611	. . 3 ⊢ (x = A → ((⟨x, B⟩ = ⟨C, D⟩ → B = D) ↔ (⟨A, B⟩ = ⟨C, D⟩ → B = D)))
4		visset 1804	. . . . 5 ⊢ x ∈ V
5		opth2.1	. . . . 5 ⊢ B ∈ V
6		opth2.2	. . . . 5 ⊢ D ∈ V
7	4, 5, 6	opth 2777	. . . 4 ⊢ (⟨x, B⟩ = ⟨C, D⟩ ↔ (x = C ⋀ B = D))
8	7	pm3.27bi 326	. . 3 ⊢ (⟨x, B⟩ = ⟨C, D⟩ → B = D)
9	3, 8	vtoclg 1838	. 2 ⊢ (A ∈ V → (⟨A, B⟩ = ⟨C, D⟩ → B = D))
10		nelneq2 1554	. . . . 5 ⊢ ((∅ ∈ ⟨A, B⟩ ⋀ ¬ ∅ ∈ ⟨C, D⟩) → ¬ ⟨A, B⟩ = ⟨C, D⟩)
11		opprc1b 2786	. . . . 5 ⊢ (¬ A ∈ V ↔ ∅ ∈ ⟨A, B⟩)
12		opprc1b 2786	. . . . . . 7 ⊢ (¬ C ∈ V ↔ ∅ ∈ ⟨C, D⟩)
13	12	con1bii 220	. . . . . 6 ⊢ (¬ ∅ ∈ ⟨C, D⟩ ↔ C ∈ V)
14	13	bicomi 172	. . . . 5 ⊢ (C ∈ V ↔ ¬ ∅ ∈ ⟨C, D⟩)
15	10, 11, 14	syl2anb 455	. . . 4 ⊢ ((¬ A ∈ V ⋀ C ∈ V) → ¬ ⟨A, B⟩ = ⟨C, D⟩)
16	15	pm2.21d 78	. . 3 ⊢ ((¬ A ∈ V ⋀ C ∈ V) → (⟨A, B⟩ = ⟨C, D⟩ → B = D))
17		opprc1 2489	. . . . 5 ⊢ (¬ A ∈ V → ⟨A, B⟩ = {∅, {B}})
18		opprc1 2489	. . . . 5 ⊢ (¬ C ∈ V → ⟨C, D⟩ = {∅, {D}})
19	17, 18	eqeqan12d 1482	. . . 4 ⊢ ((¬ A ∈ V ⋀ ¬ C ∈ V) → (⟨A, B⟩ = ⟨C, D⟩ ↔ {∅, {B}} = {∅, {D}}))
20		snex 2740	. . . . . 6 ⊢ {B} ∈ V
21		snex 2740	. . . . . 6 ⊢ {D} ∈ V
22	20, 21	preqr2 2473	. . . . 5 ⊢ ({∅, {B}} = {∅, {D}} → {B} = {D})
23	5	sneqr 2468	. . . . 5 ⊢ ({B} = {D} → B = D)
24	22, 23	syl 10	. . . 4 ⊢ ({∅, {B}} = {∅, {D}} → B = D)
25	19, 24	syl6bi 214	. . 3 ⊢ ((¬ A ∈ V ⋀ ¬ C ∈ V) → (⟨A, B⟩ = ⟨C, D⟩ → B = D))
26	16, 25	pm2.61dan 476	. 2 ⊢ (¬ A ∈ V → (⟨A, B⟩ = ⟨C, D⟩ → B = D))
27	9, 26	pm2.61i 126	1 ⊢ (⟨A, B⟩ = ⟨C, D⟩ → B = D)

Syntax hints:  ¬ wn 2   → wi 3   ⋀ wa 223   = wceq 953   ∈ wcel 955  Vcvv 1802  ∅c0 2270  {csn 2399  {cpr 2400  ⟨cop 2401

This theorem is referenced by:  moop2 2790  funsn 3529

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 959  ax-gen 960  ax-8 961  ax-10 963  ax-11 964  ax-12 965  ax-13 966  ax-14 967  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975  ax-9o 1119  ax-10o 1136  ax-16 1206  ax-11o 1213  ax-ext 1452  ax-sep 2693  ax-nul 2700  ax-pow 2732  ax-pr 2769

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 978  df-sb 1168  df-eu 1375  df-mo 1376  df-clab 1457  df-cleq 1462  df-clel 1465  df-ne 1579  df-v 1803  df-dif 2039  df-un 2040  df-in 2041  df-ss 2043  df-nul 2271  df-pw 2392  df-sn 2402  df-pr 2403  df-op 2406

Copyright terms: Public domain