Theorem opeq12 4829

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541  ⟨cop 4584

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 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4284  df-if 4478  df-sn 4579  df-pr 4581  df-op 4585

This theorem is referenced by:  opeq12i  4832  opeq12d  4835  cbvopab  5168  cbvopabv  5169  opth  5422  copsex2t  5438  relop  5797  funopg  6524  fvn0ssdmfun  7017  fsn  7078  fnressn  7101  fmptsng  7112  fmptsnd  7113  tpres  7145  cbvoprab12  7445  cbvoprab12v  7446  eqopi  7967  f1o2ndf1  8062  tposoprab  8202  omeu  8510  brecop  8745  ecovcom  8758  ecovass  8759  ecovdi  8760  xpf1o  9065  addsrmo  10982  mulsrmo  10983  addsrpr  10984  mulsrpr  10985  addcnsr  11044  axcnre  11073  seqeq1  13925  opfi1uzind  14432  fsumcnv  15694  fprodcnv  15904  eucalgval2  16506  xpstopnlem1  23751  qustgplem  24063  finsumvtxdg2size  29573  brabgaf  32633  qqhval2  34088  brsegle  36251  copsex2d  37283  finxpreclem3  37537  eqrelf  38392  dvnprodlem1  46132  or2expropbilem1  47220  or2expropbilem2  47221  funop1  47471  ich2exprop  47659  ichnreuop  47660  ichreuopeq  47661  reuopreuprim  47714  uspgrsprf1  48335