Theorem opeq12 4807

Description: Equality theorem for ordered pairs. (Contributed by NM, 28-May-1995.)

Assertion

Ref	Expression
opeq12	⊢ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) → ⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩)

Proof of Theorem opeq12

Step	Hyp	Ref	Expression
1		opeq1 4805	. 2 ⊢ (𝐴 = 𝐶 → ⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐵⟩)
2		opeq2 4806	. 2 ⊢ (𝐵 = 𝐷 → ⟨𝐶, 𝐵⟩ = ⟨𝐶, 𝐷⟩)
3	1, 2	sylan9eq 2878	1 ⊢ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) → ⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩)

Syntax hints:   → wi 4   ∧ wa 398   = wceq 1537  ⟨cop 4575

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-rab 3149  df-v 3498  df-dif 3941  df-un 3943  df-in 3945  df-ss 3954  df-nul 4294  df-if 4470  df-sn 4570  df-pr 4572  df-op 4576

This theorem is referenced by:  opeq12i  4810  opeq12d  4813  cbvopab  5139  opth  5370  copsex2t  5385  copsex2g  5386  relop  5723  funopg  6391  fvn0ssdmfun  6844  fsn  6899  fnressn  6922  fmptsng  6932  fmptsnd  6933  tpres  6965  cbvoprab12  7245  eqopi  7727  f1o2ndf1  7820  tposoprab  7930  omeu  8213  brecop  8392  ecovcom  8405  ecovass  8406  ecovdi  8407  xpf1o  8681  addsrmo  10497  mulsrmo  10498  addsrpr  10499  mulsrpr  10500  addcnsr  10559  axcnre  10588  seqeq1  13375  opfi1uzind  13862  fsumcnv  15130  fprodcnv  15339  eucalgval2  15927  xpstopnlem1  22419  qustgplem  22731  finsumvtxdg2size  27334  brabgaf  30361  qqhval2  31225  brsegle  33571  copsex2d  34433  finxpreclem3  34676  eqrelf  35519  dvnprodlem1  42238  or2expropbilem1  43274  or2expropbilem2  43275  funop1  43489  ich2exprop  43640  ichnreuop  43641  ichreuopeq  43642  reuopreuprim  43695  uspgrsprf1  44029