Theorem opthg 5461

Description: Ordered pair theorem. 𝐶 and 𝐷 are not required to be sets under our specific ordered pair definition. (Contributed by NM, 14-Oct-2005.) (Revised by Mario Carneiro, 26-Apr-2015.)

Assertion

Ref	Expression
opthg	⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷)))

Proof of Theorem opthg

Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		opeq1 4840	. . . 4 ⊢ (𝑥 = 𝐴 → ⟨𝑥, 𝑦⟩ = ⟨𝐴, 𝑦⟩)
2	1	eqeq1d 2767	. . 3 ⊢ (𝑥 = 𝐴 → (⟨𝑥, 𝑦⟩ = ⟨𝐶, 𝐷⟩ ↔ ⟨𝐴, 𝑦⟩ = ⟨𝐶, 𝐷⟩))
3		eqeq1 2769	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 = 𝐶 ↔ 𝐴 = 𝐶))
4	3	anbi1d 643	. . 3 ⊢ (𝑥 = 𝐴 → ((𝑥 = 𝐶 ∧ 𝑦 = 𝐷) ↔ (𝐴 = 𝐶 ∧ 𝑦 = 𝐷)))
5	2, 4	bibi12d 348	. 2 ⊢ (𝑥 = 𝐴 → ((⟨𝑥, 𝑦⟩ = ⟨𝐶, 𝐷⟩ ↔ (𝑥 = 𝐶 ∧ 𝑦 = 𝐷)) ↔ (⟨𝐴, 𝑦⟩ = ⟨𝐶, 𝐷⟩ ↔ (𝐴 = 𝐶 ∧ 𝑦 = 𝐷))))
6		opeq2 4841	. . . 4 ⊢ (𝑦 = 𝐵 → ⟨𝐴, 𝑦⟩ = ⟨𝐴, 𝐵⟩)
7	6	eqeq1d 2767	. . 3 ⊢ (𝑦 = 𝐵 → (⟨𝐴, 𝑦⟩ = ⟨𝐶, 𝐷⟩ ↔ ⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩))
8		eqeq1 2769	. . . 4 ⊢ (𝑦 = 𝐵 → (𝑦 = 𝐷 ↔ 𝐵 = 𝐷))
9	8	anbi2d 642	. . 3 ⊢ (𝑦 = 𝐵 → ((𝐴 = 𝐶 ∧ 𝑦 = 𝐷) ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷)))
10	7, 9	bibi12d 348	. 2 ⊢ (𝑦 = 𝐵 → ((⟨𝐴, 𝑦⟩ = ⟨𝐶, 𝐷⟩ ↔ (𝐴 = 𝐶 ∧ 𝑦 = 𝐷)) ↔ (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷))))
11		vex 3461	. . 3 ⊢ 𝑥 ∈ V
12		vex 3461	. . 3 ⊢ 𝑦 ∈ V
13	11, 12	opth 5460	. 2 ⊢ (⟨𝑥, 𝑦⟩ = ⟨𝐶, 𝐷⟩ ↔ (𝑥 = 𝐶 ∧ 𝑦 = 𝐷))
14	5, 10, 13	vtocl2g 3540	1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷)))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1570   ∈ wcel 2146  ⟨cop 4597

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737  ax-sep 5259  ax-pr 5406

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598

This theorem is used by:  opth1g  5462  opthg2  5463  opthneg  5465  otthg  5469  oteqex  5485  s111  14675  embedsetcestrclem  18237  symg2bas  19509  frgpnabllem1  19989  frgpnabllem2  19990  mat1dimbas  22681  linds2eq  33760  selvply1rhmlema  33974  selvply1rhmlem1  33976  selvply1rhmlem2  33977  goeleq12bg  35880  opideq  39052  dvheveccl  41946  hoidmv1le  47368  oppr  47827  opprb  47828  fsetsnf1  47849  prproropf1olem4  48315  fuco2  50160