Theorem opeq12 4835

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540  ⟨cop 4591

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3403  df-v 3446  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592

This theorem is referenced by:  opeq12i  4838  opeq12d  4841  cbvopab  5174  cbvopabv  5175  opth  5431  copsex2t  5447  relop  5804  funopg  6534  fvn0ssdmfun  7028  fsn  7089  fnressn  7112  fmptsng  7124  fmptsnd  7125  tpres  7157  cbvoprab12  7458  cbvoprab12v  7459  eqopi  7983  f1o2ndf1  8078  tposoprab  8218  omeu  8526  brecop  8760  ecovcom  8773  ecovass  8774  ecovdi  8775  xpf1o  9080  addsrmo  11002  mulsrmo  11003  addsrpr  11004  mulsrpr  11005  addcnsr  11064  axcnre  11093  seqeq1  13945  opfi1uzind  14452  fsumcnv  15715  fprodcnv  15925  eucalgval2  16527  xpstopnlem1  23672  qustgplem  23984  finsumvtxdg2size  29454  brabgaf  32509  qqhval2  33945  brsegle  36069  copsex2d  37100  finxpreclem3  37354  eqrelf  38217  dvnprodlem1  45917  or2expropbilem1  47006  or2expropbilem2  47007  funop1  47257  ich2exprop  47445  ichnreuop  47446  ichreuopeq  47447  reuopreuprim  47500  uspgrsprf1  48108