Theorem opeq12 4819

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542  ⟨cop 4574

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575

This theorem is referenced by:  opeq12i  4822  opeq12d  4825  cbvopab  5158  cbvopabv  5159  opth  5425  copsex2t  5441  relop  5800  funopg  6527  fvn0ssdmfun  7021  fsn  7083  fnressn  7106  fmptsng  7117  fmptsnd  7118  tpres  7150  cbvoprab12  7450  cbvoprab12v  7451  eqopi  7972  f1o2ndf1  8066  tposoprab  8206  omeu  8514  brecop  8751  ecovcom  8764  ecovass  8765  ecovdi  8766  xpf1o  9071  addsrmo  10990  mulsrmo  10991  addsrpr  10992  mulsrpr  10993  addcnsr  11052  axcnre  11081  seqeq1  13960  opfi1uzind  14467  fsumcnv  15729  fprodcnv  15942  eucalgval2  16544  xpstopnlem1  23787  qustgplem  24099  finsumvtxdg2size  29637  brabgaf  32697  qqhval2  34145  brsegle  36309  copsex2d  37472  finxpreclem3  37726  eqrelf  38596  dvnprodlem1  46395  or2expropbilem1  47495  or2expropbilem2  47496  funop1  47746  ich2exprop  47946  ichnreuop  47947  ichreuopeq  47948  reuopreuprim  48001  uspgrsprf1  48638