Theorem opeq12 4826

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

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

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701

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 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3395  df-v 3438  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584

This theorem is referenced by:  opeq12i  4829  opeq12d  4832  cbvopab  5164  cbvopabv  5165  opth  5419  copsex2t  5435  relop  5793  funopg  6516  fvn0ssdmfun  7008  fsn  7069  fnressn  7092  fmptsng  7104  fmptsnd  7105  tpres  7137  cbvoprab12  7438  cbvoprab12v  7439  eqopi  7960  f1o2ndf1  8055  tposoprab  8195  omeu  8503  brecop  8737  ecovcom  8750  ecovass  8751  ecovdi  8752  xpf1o  9056  addsrmo  10967  mulsrmo  10968  addsrpr  10969  mulsrpr  10970  addcnsr  11029  axcnre  11058  seqeq1  13911  opfi1uzind  14418  fsumcnv  15680  fprodcnv  15890  eucalgval2  16492  xpstopnlem1  23694  qustgplem  24006  finsumvtxdg2size  29496  brabgaf  32553  qqhval2  33949  brsegle  36082  copsex2d  37113  finxpreclem3  37367  eqrelf  38230  dvnprodlem1  45927  or2expropbilem1  47016  or2expropbilem2  47017  funop1  47267  ich2exprop  47455  ichnreuop  47456  ichreuopeq  47457  reuopreuprim  47510  uspgrsprf1  48131