Theorem opeq12 4844

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

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1567  ⟨cop 4600

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-ss 3930  df-nul 4295  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601

This theorem is referenced by:  opeq12i  4847  opeq12d  4850  cbvopab  5187  cbvopabv  5188  opth  5459  copsex2t  5476  relop  5837  funopg  6571  fvn0ssdmfun  7070  fsn  7132  fnressn  7156  fmptsng  7167  fmptsnd  7168  tpres  7200  cbvoprab12  7500  cbvoprab12v  7501  eqopi  8021  f1o2ndf1  8116  tposoprab  8257  omeu  8569  brecop  8807  ecovcom  8820  ecovass  8821  ecovdi  8822  xpf1o  9126  addsrmo  11057  mulsrmo  11058  addsrpr  11059  mulsrpr  11060  addcnsr  11119  axcnre  11148  seqeq1  14039  opfi1uzind  14547  fsumcnv  15823  fprodcnv  16036  eucalgval2  16638  xpstopnlem1  23934  qustgplem  24246  finsumvtxdg2size  29840  brabgaf  32891  qqhval2  34316  brsegle  36498  copsex2d  37670  finxpreclem3  37926  eqrelf  38796  dvnprodlem1  46551  or2expropbilem1  47657  or2expropbilem2  47658  funop1  47908  ich2exprop  48108  ichnreuop  48109  ichreuopeq  48110  reuopreuprim  48163  uspgrsprf1  48800