Theorem opthg 5459

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 4838	. . . 4 ⊢ (𝑥 = 𝐴 → ⟨𝑥, 𝑦⟩ = ⟨𝐴, 𝑦⟩)
2	1	eqeq1d 2765	. . 3 ⊢ (𝑥 = 𝐴 → (⟨𝑥, 𝑦⟩ = ⟨𝐶, 𝐷⟩ ↔ ⟨𝐴, 𝑦⟩ = ⟨𝐶, 𝐷⟩))
3		eqeq1 2767	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 = 𝐶 ↔ 𝐴 = 𝐶))
4	3	anbi1d 642	. . 3 ⊢ (𝑥 = 𝐴 → ((𝑥 = 𝐶 ∧ 𝑦 = 𝐷) ↔ (𝐴 = 𝐶 ∧ 𝑦 = 𝐷)))
5	2, 4	bibi12d 348	. 2 ⊢ (𝑥 = 𝐴 → ((⟨𝑥, 𝑦⟩ = ⟨𝐶, 𝐷⟩ ↔ (𝑥 = 𝐶 ∧ 𝑦 = 𝐷)) ↔ (⟨𝐴, 𝑦⟩ = ⟨𝐶, 𝐷⟩ ↔ (𝐴 = 𝐶 ∧ 𝑦 = 𝐷))))
6		opeq2 4839	. . . 4 ⊢ (𝑦 = 𝐵 → ⟨𝐴, 𝑦⟩ = ⟨𝐴, 𝐵⟩)
7	6	eqeq1d 2765	. . 3 ⊢ (𝑦 = 𝐵 → (⟨𝐴, 𝑦⟩ = ⟨𝐶, 𝐷⟩ ↔ ⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩))
8		eqeq1 2767	. . . 4 ⊢ (𝑦 = 𝐵 → (𝑦 = 𝐷 ↔ 𝐵 = 𝐷))
9	8	anbi2d 641	. . 3 ⊢ (𝑦 = 𝐵 → ((𝐴 = 𝐶 ∧ 𝑦 = 𝐷) ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷)))
10	7, 9	bibi12d 348	. 2 ⊢ (𝑦 = 𝐵 → ((⟨𝐴, 𝑦⟩ = ⟨𝐶, 𝐷⟩ ↔ (𝐴 = 𝐶 ∧ 𝑦 = 𝐷)) ↔ (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷))))
11		vex 3459	. . 3 ⊢ 𝑥 ∈ V
12		vex 3459	. . 3 ⊢ 𝑦 ∈ V
13	11, 12	opth 5458	. 2 ⊢ (⟨𝑥, 𝑦⟩ = ⟨𝐶, 𝐷⟩ ↔ (𝑥 = 𝐶 ∧ 𝑦 = 𝐷))
14	5, 10, 13	vtocl2g 3538	1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷)))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400   = wceq 1570   ∈ wcel 2143  ⟨cop 4595

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-sep 5257  ax-pr 5404

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4488  df-sn 4590  df-pr 4592  df-op 4596

This theorem is referenced by:  opth1g  5460  opthg2  5461  opthneg  5463  otthg  5467  oteqex  5483  s111  14649  embedsetcestrclem  18208  symg2bas  19458  frgpnabllem1  19938  frgpnabllem2  19939  mat1dimbas  22629  linds2eq  33694  selvply1rhmlema  33908  selvply1rhmlem1  33910  selvply1rhmlem2  33911  goeleq12bg  35841  opideq  39012  dvheveccl  41906  hoidmv1le  47328  oppr  47787  opprb  47788  fsetsnf1  47809  prproropf1olem4  48275  fuco2  50121