MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  opthg Structured version   Visualization version   GIF version

Theorem opthg 5481
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.
StepHypRef Expression
1 opeq1 4872 . . . 4 (𝑥 = 𝐴 → ⟨𝑥, 𝑦⟩ = ⟨𝐴, 𝑦⟩)
21eqeq1d 2738 . . 3 (𝑥 = 𝐴 → (⟨𝑥, 𝑦⟩ = ⟨𝐶, 𝐷⟩ ↔ ⟨𝐴, 𝑦⟩ = ⟨𝐶, 𝐷⟩))
3 eqeq1 2740 . . . 4 (𝑥 = 𝐴 → (𝑥 = 𝐶𝐴 = 𝐶))
43anbi1d 631 . . 3 (𝑥 = 𝐴 → ((𝑥 = 𝐶𝑦 = 𝐷) ↔ (𝐴 = 𝐶𝑦 = 𝐷)))
52, 4bibi12d 345 . 2 (𝑥 = 𝐴 → ((⟨𝑥, 𝑦⟩ = ⟨𝐶, 𝐷⟩ ↔ (𝑥 = 𝐶𝑦 = 𝐷)) ↔ (⟨𝐴, 𝑦⟩ = ⟨𝐶, 𝐷⟩ ↔ (𝐴 = 𝐶𝑦 = 𝐷))))
6 opeq2 4873 . . . 4 (𝑦 = 𝐵 → ⟨𝐴, 𝑦⟩ = ⟨𝐴, 𝐵⟩)
76eqeq1d 2738 . . 3 (𝑦 = 𝐵 → (⟨𝐴, 𝑦⟩ = ⟨𝐶, 𝐷⟩ ↔ ⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩))
8 eqeq1 2740 . . . 4 (𝑦 = 𝐵 → (𝑦 = 𝐷𝐵 = 𝐷))
98anbi2d 630 . . 3 (𝑦 = 𝐵 → ((𝐴 = 𝐶𝑦 = 𝐷) ↔ (𝐴 = 𝐶𝐵 = 𝐷)))
107, 9bibi12d 345 . 2 (𝑦 = 𝐵 → ((⟨𝐴, 𝑦⟩ = ⟨𝐶, 𝐷⟩ ↔ (𝐴 = 𝐶𝑦 = 𝐷)) ↔ (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ ↔ (𝐴 = 𝐶𝐵 = 𝐷))))
11 vex 3483 . . 3 𝑥 ∈ V
12 vex 3483 . . 3 𝑦 ∈ V
1311, 12opth 5480 . 2 (⟨𝑥, 𝑦⟩ = ⟨𝐶, 𝐷⟩ ↔ (𝑥 = 𝐶𝑦 = 𝐷))
145, 10, 13vtocl2g 3573 1 ((𝐴𝑉𝐵𝑊) → (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ ↔ (𝐴 = 𝐶𝐵 = 𝐷)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395   = wceq 1539  wcel 2107  cop 4631
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2707  ax-sep 5295  ax-nul 5305  ax-pr 5431
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-rab 3436  df-v 3481  df-dif 3953  df-un 3955  df-ss 3967  df-nul 4333  df-if 4525  df-sn 4626  df-pr 4628  df-op 4632
This theorem is referenced by:  opth1g  5482  opthg2  5483  opthneg  5485  otthg  5489  oteqex  5504  s111  14654  embedsetcestrclem  18203  symg2bas  19411  frgpnabllem1  19892  frgpnabllem2  19893  mat1dimbas  22479  linds2eq  33410  goeleq12bg  35355  opideq  38345  dvheveccl  41115  hoidmv1le  46614  oppr  47047  opprb  47048  fsetsnf1  47069  prproropf1olem4  47498  fuco2  49041
  Copyright terms: Public domain W3C validator