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 2792	1 ⊢ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) → ⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩)

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

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 3402  df-v 3444  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589

This theorem is referenced by:  opeq12i  4836  opeq12d  4839  cbvopab  5172  cbvopabv  5173  opth  5432  copsex2t  5448  relop  5807  funopg  6534  fvn0ssdmfun  7028  fsn  7090  fnressn  7113  fmptsng  7124  fmptsnd  7125  tpres  7157  cbvoprab12  7457  cbvoprab12v  7458  eqopi  7979  f1o2ndf1  8074  tposoprab  8214  omeu  8522  brecop  8759  ecovcom  8772  ecovass  8773  ecovdi  8774  xpf1o  9079  addsrmo  10996  mulsrmo  10997  addsrpr  10998  mulsrpr  10999  addcnsr  11058  axcnre  11087  seqeq1  13939  opfi1uzind  14446  fsumcnv  15708  fprodcnv  15918  eucalgval2  16520  xpstopnlem1  23765  qustgplem  24077  finsumvtxdg2size  29636  brabgaf  32696  qqhval2  34160  brsegle  36324  copsex2d  37394  finxpreclem3  37648  eqrelf  38509  dvnprodlem1  46304  or2expropbilem1  47392  or2expropbilem2  47393  funop1  47643  ich2exprop  47831  ichnreuop  47832  ichreuopeq  47833  reuopreuprim  47886  uspgrsprf1  48507