Theorem opeq12 4875

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

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

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633

This theorem is referenced by:  opeq12i  4878  opeq12d  4881  cbvopab  5215  cbvopabv  5216  opth  5481  copsex2t  5497  relop  5861  funopg  6600  fvn0ssdmfun  7094  fsn  7155  fnressn  7178  fmptsng  7188  fmptsnd  7189  tpres  7221  cbvoprab12  7522  cbvoprab12v  7523  eqopi  8050  f1o2ndf1  8147  tposoprab  8287  omeu  8623  brecop  8850  ecovcom  8863  ecovass  8864  ecovdi  8865  xpf1o  9179  addsrmo  11113  mulsrmo  11114  addsrpr  11115  mulsrpr  11116  addcnsr  11175  axcnre  11204  seqeq1  14045  opfi1uzind  14550  fsumcnv  15809  fprodcnv  16019  eucalgval2  16618  xpstopnlem1  23817  qustgplem  24129  finsumvtxdg2size  29568  brabgaf  32620  qqhval2  33983  brsegle  36109  copsex2d  37140  finxpreclem3  37394  eqrelf  38256  dvnprodlem1  45961  or2expropbilem1  47044  or2expropbilem2  47045  funop1  47295  ich2exprop  47458  ichnreuop  47459  ichreuopeq  47460  reuopreuprim  47513  uspgrsprf1  48063