Theorem opeq12 4812

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

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1542  ⟨cop 4573

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-8 2112  ax-9 2120  ax-ext 2711

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1545  df-fal 1555  df-ex 1787  df-sb 2072  df-clab 2718  df-cleq 2732  df-clel 2818  df-rab 3075  df-v 3433  df-dif 3895  df-un 3897  df-nul 4263  df-if 4466  df-sn 4568  df-pr 4570  df-op 4574

This theorem is referenced by:  opeq12i  4815  opeq12d  4818  cbvopab  5151  cbvopabv  5152  opth  5395  copsex2t  5410  copsex2gOLD  5412  relop  5758  funopg  6466  fvn0ssdmfun  6949  fsn  7004  fnressn  7027  fmptsng  7037  fmptsnd  7038  tpres  7073  cbvoprab12  7358  eqopi  7860  f1o2ndf1  7954  tposoprab  8069  omeu  8401  brecop  8582  ecovcom  8595  ecovass  8596  ecovdi  8597  xpf1o  8908  addsrmo  10830  mulsrmo  10831  addsrpr  10832  mulsrpr  10833  addcnsr  10892  axcnre  10921  seqeq1  13722  opfi1uzind  14213  fsumcnv  15483  fprodcnv  15691  eucalgval2  16284  xpstopnlem1  22958  qustgplem  23270  finsumvtxdg2size  27915  brabgaf  30944  qqhval2  31928  brsegle  34406  copsex2d  35306  finxpreclem3  35560  eqrelf  36391  dvnprodlem1  43458  or2expropbilem1  44494  or2expropbilem2  44495  funop1  44743  ich2exprop  44892  ichnreuop  44893  ichreuopeq  44894  reuopreuprim  44947  uspgrsprf1  45278