Theorem opeq12 4543

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

Syntax hints:   → wi 4   ∧ wa 383   = wceq 1620  ⟨cop 4315

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1859  ax-4 1874  ax-5 1976  ax-6 2042  ax-7 2078  ax-9 2136  ax-10 2156  ax-11 2171  ax-12 2184  ax-13 2379  ax-ext 2728

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1623  df-ex 1842  df-nf 1847  df-sb 2035  df-clab 2735  df-cleq 2741  df-clel 2744  df-nfc 2879  df-rab 3047  df-v 3330  df-dif 3706  df-un 3708  df-in 3710  df-ss 3717  df-nul 4047  df-if 4219  df-sn 4310  df-pr 4312  df-op 4316

This theorem is referenced by:  opeq12i  4546  opeq12d  4549  cbvopab  4861  opth  5081  copsex2t  5093  copsex2g  5094  relop  5416  funopg  6071  fvn0ssdmfun  6501  fsn  6553  fnressn  6576  fmptsng  6586  fmptsnd  6587  tpres  6618  cbvoprab12  6882  eqopi  7357  f1o2ndf1  7441  tposoprab  7545  omeu  7822  brecop  7995  ecovcom  8008  ecovass  8009  ecovdi  8010  xpf1o  8275  addsrmo  10057  mulsrmo  10058  addsrpr  10059  mulsrpr  10060  addcnsr  10119  axcnre  10148  seqeq1  12969  opfi1uzind  13446  fsumcnv  14674  fprodcnv  14883  eucalgval2  15467  xpstopnlem1  21785  qustgplem  22096  finsumvtxdg2size  26627  brabgaf  29698  qqhval2  30306  brsegle  32492  finxpreclem3  33512  eqrelf  34313  dvnprodlem1  40633  funop1  41779  uspgrsprf1  42234