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

Theorem opth2 4721
Description: Ordered pair theorem. (Contributed by NM, 21-Sep-2014.)
Hypotheses
Ref Expression
opth2.1 𝐶 ∈ V
opth2.2 𝐷 ∈ V
Assertion
Ref Expression
opth2 (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ ↔ (𝐴 = 𝐶𝐵 = 𝐷))

Proof of Theorem opth2
StepHypRef Expression
1 opth2.1 . 2 𝐶 ∈ V
2 opth2.2 . 2 𝐷 ∈ V
3 opthg2 4720 . 2 ((𝐶 ∈ V ∧ 𝐷 ∈ V) → (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ ↔ (𝐴 = 𝐶𝐵 = 𝐷)))
41, 2, 3mp2an 695 1 (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ ↔ (𝐴 = 𝐶𝐵 = 𝐷))
Colors of variables: wff setvar class
Syntax hints:  wb 191  wa 378   = wceq 1468  wcel 1937  Vcvv 3066  cop 4001
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1698  ax-4 1711  ax-5 1789  ax-6 1836  ax-7 1883  ax-9 1946  ax-10 1965  ax-11 1970  ax-12 1983  ax-13 2137  ax-ext 2485  ax-sep 4558  ax-nul 4567  ax-pr 4680
This theorem depends on definitions:  df-bi 192  df-or 379  df-an 380  df-3an 1023  df-tru 1471  df-ex 1693  df-nf 1697  df-sb 1829  df-clab 2492  df-cleq 2498  df-clel 2501  df-nfc 2635  df-ne 2677  df-rab 2800  df-v 3068  df-dif 3429  df-un 3431  df-in 3433  df-ss 3440  df-nul 3758  df-if 3909  df-sn 3996  df-pr 3998  df-op 4002
This theorem is referenced by:  eqvinop  4727  opelxp  4910  fsn  6129  opiota  6929  canthwe  9161  ltresr  9649  mat1dimelbas  19654  fmucndlem  21464  diblsmopel  34979  cdlemn7  35011  dihordlem7  35022  xihopellsmN  35062  dihopellsm  35063  dihpN  35144
  Copyright terms: Public domain W3C validator