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

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

Proof of Theorem opeq12
StepHypRef Expression
1 opeq1 4763 . 2 (𝐴 = 𝐶 → ⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐵⟩)
2 opeq2 4765 . 2 (𝐵 = 𝐷 → ⟨𝐶, 𝐵⟩ = ⟨𝐶, 𝐷⟩)
31, 2sylan9eq 2853 1 ((𝐴 = 𝐶𝐵 = 𝐷) → ⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399   = wceq 1538  ⟨cop 4531 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-un 3886  df-sn 4526  df-pr 4528  df-op 4532 This theorem is referenced by:  opeq12i  4770  opeq12d  4773  cbvopab  5101  opth  5333  copsex2t  5348  copsex2g  5349  relop  5685  funopg  6358  fvn0ssdmfun  6819  fsn  6874  fnressn  6897  fmptsng  6907  fmptsnd  6908  tpres  6940  cbvoprab12  7222  eqopi  7709  f1o2ndf1  7803  tposoprab  7913  omeu  8196  brecop  8375  ecovcom  8388  ecovass  8389  ecovdi  8390  xpf1o  8665  addsrmo  10486  mulsrmo  10487  addsrpr  10488  mulsrpr  10489  addcnsr  10548  axcnre  10577  seqeq1  13369  opfi1uzind  13857  fsumcnv  15122  fprodcnv  15331  eucalgval2  15917  xpstopnlem1  22421  qustgplem  22733  finsumvtxdg2size  27347  brabgaf  30379  qqhval2  31345  brsegle  33694  copsex2d  34570  finxpreclem3  34826  eqrelf  35693  dvnprodlem1  42603  or2expropbilem1  43639  or2expropbilem2  43640  funop1  43854  ich2exprop  44003  ichnreuop  44004  ichreuopeq  44005  reuopreuprim  44058  uspgrsprf1  44390
 Copyright terms: Public domain W3C validator