Theorem opeq12 4839

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

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

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 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596

This theorem is referenced by:  opeq12i  4842  opeq12d  4845  cbvopab  5179  cbvopabv  5180  opth  5436  copsex2t  5452  relop  5814  funopg  6550  fvn0ssdmfun  7046  fsn  7107  fnressn  7130  fmptsng  7142  fmptsnd  7143  tpres  7175  cbvoprab12  7478  cbvoprab12v  7479  eqopi  8004  f1o2ndf1  8101  tposoprab  8241  omeu  8549  brecop  8783  ecovcom  8796  ecovass  8797  ecovdi  8798  xpf1o  9103  addsrmo  11026  mulsrmo  11027  addsrpr  11028  mulsrpr  11029  addcnsr  11088  axcnre  11117  seqeq1  13969  opfi1uzind  14476  fsumcnv  15739  fprodcnv  15949  eucalgval2  16551  xpstopnlem1  23696  qustgplem  24008  finsumvtxdg2size  29478  brabgaf  32536  qqhval2  33972  brsegle  36096  copsex2d  37127  finxpreclem3  37381  eqrelf  38244  dvnprodlem1  45944  or2expropbilem1  47033  or2expropbilem2  47034  funop1  47284  ich2exprop  47472  ichnreuop  47473  ichreuopeq  47474  reuopreuprim  47527  uspgrsprf1  48135