Theorem opeq12 4803

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1539  ⟨cop 4564

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565

This theorem is referenced by:  opeq12i  4806  opeq12d  4809  cbvopab  5142  cbvopabv  5143  opth  5385  copsex2t  5400  copsex2gOLD  5402  relop  5748  funopg  6452  fvn0ssdmfun  6934  fsn  6989  fnressn  7012  fmptsng  7022  fmptsnd  7023  tpres  7058  cbvoprab12  7342  eqopi  7840  f1o2ndf1  7934  tposoprab  8049  omeu  8378  brecop  8557  ecovcom  8570  ecovass  8571  ecovdi  8572  xpf1o  8875  addsrmo  10760  mulsrmo  10761  addsrpr  10762  mulsrpr  10763  addcnsr  10822  axcnre  10851  seqeq1  13652  opfi1uzind  14143  fsumcnv  15413  fprodcnv  15621  eucalgval2  16214  xpstopnlem1  22868  qustgplem  23180  finsumvtxdg2size  27820  brabgaf  30849  qqhval2  31832  brsegle  34337  copsex2d  35237  finxpreclem3  35491  eqrelf  36322  dvnprodlem1  43377  or2expropbilem1  44413  or2expropbilem2  44414  funop1  44662  ich2exprop  44811  ichnreuop  44812  ichreuopeq  44813  reuopreuprim  44866  uspgrsprf1  45197