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

Theorem opeq12 4342
 Description: Equality theorem for ordered pairs. (Contributed by NM, 28-May-1995.)
Assertion
Ref Expression
opeq12 ((𝐴 = 𝐶𝐵 = 𝐷) → ⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩)

Proof of Theorem opeq12
StepHypRef Expression
1 opeq1 4340 . 2 (𝐴 = 𝐶 → ⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐵⟩)
2 opeq2 4341 . 2 (𝐵 = 𝐷 → ⟨𝐶, 𝐵⟩ = ⟨𝐶, 𝐷⟩)
31, 2sylan9eq 2664 1 ((𝐴 = 𝐶𝐵 = 𝐷) → ⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 383   = wceq 1475  ⟨cop 4131 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132 This theorem is referenced by:  opeq12i  4345  opeq12d  4348  cbvopab  4653  opth  4871  copsex2t  4883  copsex2g  4884  relop  5194  funopg  5836  fvn0ssdmfun  6258  fsn  6308  fnressn  6330  fmptsng  6339  fmptsnd  6340  tpres  6371  cbvoprab12  6627  eqopi  7093  f1o2ndf1  7172  tposoprab  7275  omeu  7552  brecop  7727  ecovcom  7741  ecovass  7742  ecovdi  7743  xpf1o  8007  addsrmo  9773  mulsrmo  9774  addsrpr  9775  mulsrpr  9776  addcnsr  9835  axcnre  9864  seqeq1  12666  opfi1uzind  13138  opfi1uzindOLD  13144  fsumcnv  14346  fprodcnv  14552  eucalgval2  15132  xpstopnlem1  21422  qustgplem  21734  isrusgra  26454  brabgaf  28800  qqhval2  29354  brsegle  31385  finxpreclem3  32406  dvnprodlem1  38836  funop1  40327
 Copyright terms: Public domain W3C validator