Theorem opeq12 4828

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584

This theorem is referenced by:  opeq12i  4831  opeq12d  4834  cbvopab  5167  cbvopabv  5168  opth  5421  copsex2t  5437  relop  5797  funopg  6523  fvn0ssdmfun  7016  fsn  7077  fnressn  7100  fmptsng  7111  fmptsnd  7112  tpres  7144  cbvoprab12  7444  cbvoprab12v  7445  eqopi  7966  f1o2ndf1  8061  tposoprab  8201  omeu  8509  brecop  8743  ecovcom  8756  ecovass  8757  ecovdi  8758  xpf1o  9062  addsrmo  10974  mulsrmo  10975  addsrpr  10976  mulsrpr  10977  addcnsr  11036  axcnre  11065  seqeq1  13921  opfi1uzind  14428  fsumcnv  15690  fprodcnv  15900  eucalgval2  16502  xpstopnlem1  23734  qustgplem  24046  finsumvtxdg2size  29540  brabgaf  32600  qqhval2  34006  brsegle  36163  copsex2d  37194  finxpreclem3  37448  eqrelf  38302  dvnprodlem1  46058  or2expropbilem1  47146  or2expropbilem2  47147  funop1  47397  ich2exprop  47585  ichnreuop  47586  ichreuopeq  47587  reuopreuprim  47640  uspgrsprf1  48261