Theorem opeq12 4877

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

Syntax hints:   → wi 4   ∧ wa 394   = wceq 1533  ⟨cop 4636

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-rab 3419  df-v 3463  df-dif 3947  df-un 3949  df-ss 3961  df-nul 4323  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637

This theorem is referenced by:  opeq12i  4880  opeq12d  4883  cbvopab  5221  cbvopabv  5222  opth  5478  copsex2t  5494  copsex2gOLD  5496  relop  5853  funopg  6588  fvn0ssdmfun  7083  fsn  7144  fnressn  7167  fmptsng  7177  fmptsnd  7178  tpres  7213  cbvoprab12  7509  eqopi  8030  f1o2ndf1  8127  tposoprab  8268  omeu  8606  brecop  8829  ecovcom  8842  ecovass  8843  ecovdi  8844  xpf1o  9167  addsrmo  11103  mulsrmo  11104  addsrpr  11105  mulsrpr  11106  addcnsr  11165  axcnre  11194  seqeq1  14010  opfi1uzind  14503  fsumcnv  15760  fprodcnv  15968  eucalgval2  16560  xpstopnlem1  23762  qustgplem  24074  finsumvtxdg2size  29441  brabgaf  32482  qqhval2  33716  brsegle  35837  copsex2d  36751  finxpreclem3  37005  eqrelf  37859  dvnprodlem1  45474  or2expropbilem1  46554  or2expropbilem2  46555  funop1  46803  ich2exprop  46950  ichnreuop  46951  ichreuopeq  46952  reuopreuprim  47005  uspgrsprf1  47397