Theorem opeq12 4851

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540  ⟨cop 4607

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608

This theorem is referenced by:  opeq12i  4854  opeq12d  4857  cbvopab  5191  cbvopabv  5192  opth  5451  copsex2t  5467  relop  5830  funopg  6570  fvn0ssdmfun  7064  fsn  7125  fnressn  7148  fmptsng  7160  fmptsnd  7161  tpres  7193  cbvoprab12  7496  cbvoprab12v  7497  eqopi  8024  f1o2ndf1  8121  tposoprab  8261  omeu  8597  brecop  8824  ecovcom  8837  ecovass  8838  ecovdi  8839  xpf1o  9153  addsrmo  11087  mulsrmo  11088  addsrpr  11089  mulsrpr  11090  addcnsr  11149  axcnre  11178  seqeq1  14022  opfi1uzind  14529  fsumcnv  15789  fprodcnv  15999  eucalgval2  16600  xpstopnlem1  23747  qustgplem  24059  finsumvtxdg2size  29530  brabgaf  32588  qqhval2  34013  brsegle  36126  copsex2d  37157  finxpreclem3  37411  eqrelf  38273  dvnprodlem1  45975  or2expropbilem1  47061  or2expropbilem2  47062  funop1  47312  ich2exprop  47485  ichnreuop  47486  ichreuopeq  47487  reuopreuprim  47540  uspgrsprf1  48122