Theorem opeq12 4899

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1537  ⟨cop 4654

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655

This theorem is referenced by:  opeq12i  4902  opeq12d  4905  cbvopab  5238  cbvopabv  5239  opth  5496  copsex2t  5512  relop  5875  funopg  6612  fvn0ssdmfun  7108  fsn  7169  fnressn  7192  fmptsng  7202  fmptsnd  7203  tpres  7238  cbvoprab12  7539  cbvoprab12v  7540  eqopi  8066  f1o2ndf1  8163  tposoprab  8303  omeu  8641  brecop  8868  ecovcom  8881  ecovass  8882  ecovdi  8883  xpf1o  9205  addsrmo  11142  mulsrmo  11143  addsrpr  11144  mulsrpr  11145  addcnsr  11204  axcnre  11233  seqeq1  14055  opfi1uzind  14560  fsumcnv  15821  fprodcnv  16031  eucalgval2  16628  xpstopnlem1  23838  qustgplem  24150  finsumvtxdg2size  29586  brabgaf  32630  qqhval2  33928  brsegle  36072  copsex2d  37105  finxpreclem3  37359  eqrelf  38211  dvnprodlem1  45867  or2expropbilem1  46947  or2expropbilem2  46948  funop1  47198  ich2exprop  47345  ichnreuop  47346  ichreuopeq  47347  reuopreuprim  47400  uspgrsprf1  47870