Theorem opeq12 4824

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

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

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 2113  ax-9 2121  ax-ext 2703

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 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-ss 3914  df-nul 4281  df-if 4473  df-sn 4574  df-pr 4576  df-op 4580

This theorem is referenced by:  opeq12i  4827  opeq12d  4830  cbvopab  5161  cbvopabv  5162  opth  5414  copsex2t  5430  relop  5789  funopg  6515  fvn0ssdmfun  7007  fsn  7068  fnressn  7091  fmptsng  7102  fmptsnd  7103  tpres  7135  cbvoprab12  7435  cbvoprab12v  7436  eqopi  7957  f1o2ndf1  8052  tposoprab  8192  omeu  8500  brecop  8734  ecovcom  8747  ecovass  8748  ecovdi  8749  xpf1o  9052  addsrmo  10964  mulsrmo  10965  addsrpr  10966  mulsrpr  10967  addcnsr  11026  axcnre  11055  seqeq1  13911  opfi1uzind  14418  fsumcnv  15680  fprodcnv  15890  eucalgval2  16492  xpstopnlem1  23724  qustgplem  24036  finsumvtxdg2size  29529  brabgaf  32589  qqhval2  33995  brsegle  36150  copsex2d  37181  finxpreclem3  37435  eqrelf  38298  dvnprodlem1  45992  or2expropbilem1  47071  or2expropbilem2  47072  funop1  47322  ich2exprop  47510  ichnreuop  47511  ichreuopeq  47512  reuopreuprim  47565  uspgrsprf1  48186