Theorem opeq12 4806

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 4804	. 2 ⊢ (𝐴 = 𝐶 → ⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐵⟩)
2		opeq2 4805	. 2 ⊢ (𝐵 = 𝐷 → ⟨𝐶, 𝐵⟩ = ⟨𝐶, 𝐷⟩)
3	1, 2	sylan9eq 2798	1 ⊢ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) → ⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩)

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1539  ⟨cop 4567

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-rab 3073  df-v 3434  df-dif 3890  df-un 3892  df-nul 4257  df-if 4460  df-sn 4562  df-pr 4564  df-op 4568

This theorem is referenced by:  opeq12i  4809  opeq12d  4812  cbvopab  5146  cbvopabv  5147  opth  5391  copsex2t  5406  copsex2gOLD  5408  relop  5759  funopg  6468  fvn0ssdmfun  6952  fsn  7007  fnressn  7030  fmptsng  7040  fmptsnd  7041  tpres  7076  cbvoprab12  7364  eqopi  7867  f1o2ndf1  7963  tposoprab  8078  omeu  8416  brecop  8599  ecovcom  8612  ecovass  8613  ecovdi  8614  xpf1o  8926  addsrmo  10829  mulsrmo  10830  addsrpr  10831  mulsrpr  10832  addcnsr  10891  axcnre  10920  seqeq1  13724  opfi1uzind  14215  fsumcnv  15485  fprodcnv  15693  eucalgval2  16286  xpstopnlem1  22960  qustgplem  23272  finsumvtxdg2size  27917  brabgaf  30948  qqhval2  31932  brsegle  34410  copsex2d  35310  finxpreclem3  35564  eqrelf  36395  dvnprodlem1  43487  or2expropbilem1  44526  or2expropbilem2  44527  funop1  44775  ich2exprop  44923  ichnreuop  44924  ichreuopeq  44925  reuopreuprim  44978  uspgrsprf1  45309