Theorem opeq12 4872

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1534  ⟨cop 4631

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2699

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-sb 2061  df-clab 2706  df-cleq 2720  df-clel 2806  df-rab 3429  df-v 3472  df-dif 3948  df-un 3950  df-in 3952  df-ss 3962  df-nul 4320  df-if 4526  df-sn 4626  df-pr 4628  df-op 4632

This theorem is referenced by:  opeq12i  4875  opeq12d  4878  cbvopab  5215  cbvopabv  5216  opth  5473  copsex2t  5489  copsex2gOLD  5491  relop  5848  funopg  6582  fvn0ssdmfun  7079  fsn  7139  fnressn  7162  fmptsng  7172  fmptsnd  7173  tpres  7208  cbvoprab12  7504  eqopi  8024  f1o2ndf1  8122  tposoprab  8262  omeu  8600  brecop  8823  ecovcom  8836  ecovass  8837  ecovdi  8838  xpf1o  9158  addsrmo  11091  mulsrmo  11092  addsrpr  11093  mulsrpr  11094  addcnsr  11153  axcnre  11182  seqeq1  13996  opfi1uzind  14489  fsumcnv  15746  fprodcnv  15954  eucalgval2  16546  xpstopnlem1  23707  qustgplem  24019  finsumvtxdg2size  29358  brabgaf  32392  qqhval2  33578  brsegle  35699  copsex2d  36613  finxpreclem3  36867  eqrelf  37722  dvnprodlem1  45325  or2expropbilem1  46405  or2expropbilem2  46406  funop1  46654  ich2exprop  46802  ichnreuop  46803  ichreuopeq  46804  reuopreuprim  46857  uspgrsprf1  47200