Theorem opeq12 4833

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

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1560  ⟨cop 4588

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1100  df-tru 1563  df-fal 1573  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3415  df-v 3456  df-dif 3907  df-un 3909  df-ss 3921  df-nul 4286  df-if 4481  df-sn 4583  df-pr 4585  df-op 4589

This theorem is referenced by:  opeq12i  4836  opeq12d  4839  cbvopab  5172  cbvopabv  5173  opth  5444  copsex2t  5461  relop  5822  funopg  6555  fvn0ssdmfun  7055  fsn  7117  fnressn  7141  fmptsng  7152  fmptsnd  7153  tpres  7185  cbvoprab12  7485  cbvoprab12v  7486  eqopi  8006  f1o2ndf1  8101  tposoprab  8242  omeu  8554  brecop  8792  ecovcom  8805  ecovass  8806  ecovdi  8807  xpf1o  9111  addsrmo  11031  mulsrmo  11032  addsrpr  11033  mulsrpr  11034  addcnsr  11093  axcnre  11122  seqeq1  14017  opfi1uzind  14524  fsumcnv  15800  fprodcnv  16013  eucalgval2  16615  xpstopnlem1  23866  qustgplem  24178  finsumvtxdg2size  29748  brabgaf  32805  qqhval2  34276  brsegle  36455  copsex2d  37628  finxpreclem3  37884  eqrelf  38754  dvnprodlem1  46517  or2expropbilem1  47623  or2expropbilem2  47624  funop1  47874  ich2exprop  48074  ichnreuop  48075  ichreuopeq  48076  reuopreuprim  48129  uspgrsprf1  48766