Theorem opeq12 4831

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

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

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 2708

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 2715  df-cleq 2728  df-clel 2811  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587

This theorem is referenced by:  opeq12i  4834  opeq12d  4837  cbvopab  5170  cbvopabv  5171  opth  5424  copsex2t  5440  relop  5799  funopg  6526  fvn0ssdmfun  7019  fsn  7080  fnressn  7103  fmptsng  7114  fmptsnd  7115  tpres  7147  cbvoprab12  7447  cbvoprab12v  7448  eqopi  7969  f1o2ndf1  8064  tposoprab  8204  omeu  8512  brecop  8747  ecovcom  8760  ecovass  8761  ecovdi  8762  xpf1o  9067  addsrmo  10984  mulsrmo  10985  addsrpr  10986  mulsrpr  10987  addcnsr  11046  axcnre  11075  seqeq1  13927  opfi1uzind  14434  fsumcnv  15696  fprodcnv  15906  eucalgval2  16508  xpstopnlem1  23753  qustgplem  24065  finsumvtxdg2size  29624  brabgaf  32684  qqhval2  34139  brsegle  36302  copsex2d  37344  finxpreclem3  37598  eqrelf  38453  dvnprodlem1  46190  or2expropbilem1  47278  or2expropbilem2  47279  funop1  47529  ich2exprop  47717  ichnreuop  47718  ichreuopeq  47719  reuopreuprim  47772  uspgrsprf1  48393