Theorem opeq12 4836

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

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1563  ⟨cop 4591

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-rab 3418  df-v 3459  df-dif 3910  df-un 3912  df-ss 3924  df-nul 4289  df-if 4484  df-sn 4586  df-pr 4588  df-op 4592

This theorem is referenced by:  opeq12i  4839  opeq12d  4842  cbvopab  5177  cbvopabv  5178  opth  5449  copsex2t  5466  relop  5827  funopg  6559  fvn0ssdmfun  7059  fsn  7121  fnressn  7145  fmptsng  7156  fmptsnd  7157  tpres  7189  cbvoprab12  7489  cbvoprab12v  7490  eqopi  8010  f1o2ndf1  8105  tposoprab  8246  omeu  8558  brecop  8796  ecovcom  8809  ecovass  8810  ecovdi  8811  xpf1o  9115  addsrmo  11046  mulsrmo  11047  addsrpr  11048  mulsrpr  11049  addcnsr  11108  axcnre  11137  seqeq1  14031  opfi1uzind  14538  fsumcnv  15814  fprodcnv  16027  eucalgval2  16629  xpstopnlem1  23927  qustgplem  24239  finsumvtxdg2size  29809  brabgaf  32863  qqhval2  34289  brsegle  36471  copsex2d  37643  finxpreclem3  37899  eqrelf  38769  dvnprodlem1  46518  or2expropbilem1  47624  or2expropbilem2  47625  funop1  47875  ich2exprop  48075  ichnreuop  48076  ichreuopeq  48077  reuopreuprim  48130  uspgrsprf1  48767