Theorem opeq12 4840

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

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1570  ⟨cop 4595

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4488  df-sn 4590  df-pr 4592  df-op 4596

This theorem is referenced by:  opeq12i  4843  opeq12d  4846  cbvopab  5183  cbvopabv  5184  opth  5458  copsex2t  5475  relop  5836  funopg  6570  fvn0ssdmfun  7069  fsn  7131  fnressn  7155  fmptsng  7166  fmptsnd  7167  tpres  7199  cbvoprab12  7499  cbvoprab12v  7500  eqopi  8018  f1o2ndf1  8113  tposoprab  8254  omeu  8566  brecop  8804  ecovcom  8817  ecovass  8818  ecovdi  8819  xpf1o  9123  addsrmo  11053  mulsrmo  11054  addsrpr  11055  mulsrpr  11056  addcnsr  11115  axcnre  11144  seqeq1  14036  opfi1uzind  14544  fsumcnv  15820  fprodcnv  16033  eucalgval2  16634  xpstopnlem1  23966  qustgplem  24278  finsumvtxdg2size  29900  brabgaf  32951  qqhval2  34372  brsegle  36600  copsex2d  37783  finxpreclem3  38039  eqrelf  38907  dvnprodlem1  46660  or2expropbilem1  47769  or2expropbilem2  47770  funop1  48020  ich2exprop  48220  ichnreuop  48221  ichreuopeq  48222  reuopreuprim  48275  uspgrsprf1  48912