Theorem opeq12 4786

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

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1543  ⟨cop 4547

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-sb 2071  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3070  df-v 3410  df-dif 3869  df-un 3871  df-nul 4238  df-if 4440  df-sn 4542  df-pr 4544  df-op 4548

This theorem is referenced by:  opeq12i  4789  opeq12d  4792  cbvopab  5125  cbvopabv  5126  opth  5360  copsex2t  5375  copsex2gOLD  5377  relop  5719  funopg  6414  fvn0ssdmfun  6895  fsn  6950  fnressn  6973  fmptsng  6983  fmptsnd  6984  tpres  7016  cbvoprab12  7300  eqopi  7797  f1o2ndf1  7891  tposoprab  8004  omeu  8313  brecop  8492  ecovcom  8505  ecovass  8506  ecovdi  8507  xpf1o  8808  addsrmo  10687  mulsrmo  10688  addsrpr  10689  mulsrpr  10690  addcnsr  10749  axcnre  10778  seqeq1  13577  opfi1uzind  14067  fsumcnv  15337  fprodcnv  15545  eucalgval2  16138  xpstopnlem1  22706  qustgplem  23018  finsumvtxdg2size  27638  brabgaf  30667  qqhval2  31644  brsegle  34147  copsex2d  35045  finxpreclem3  35301  eqrelf  36132  dvnprodlem1  43162  or2expropbilem1  44198  or2expropbilem2  44199  funop1  44447  ich2exprop  44596  ichnreuop  44597  ichreuopeq  44598  reuopreuprim  44651  uspgrsprf1  44982