Theorem opeq12 4818

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542  ⟨cop 4573

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574

This theorem is referenced by:  opeq12i  4821  opeq12d  4824  cbvopab  5157  cbvopabv  5158  opth  5429  copsex2t  5446  relop  5805  funopg  6532  fvn0ssdmfun  7026  fsn  7088  fnressn  7112  fmptsng  7123  fmptsnd  7124  tpres  7156  cbvoprab12  7456  cbvoprab12v  7457  eqopi  7978  f1o2ndf1  8072  tposoprab  8212  omeu  8520  brecop  8757  ecovcom  8770  ecovass  8771  ecovdi  8772  xpf1o  9077  addsrmo  10996  mulsrmo  10997  addsrpr  10998  mulsrpr  10999  addcnsr  11058  axcnre  11087  seqeq1  13966  opfi1uzind  14473  fsumcnv  15735  fprodcnv  15948  eucalgval2  16550  xpstopnlem1  23774  qustgplem  24086  finsumvtxdg2size  29619  brabgaf  32679  qqhval2  34126  brsegle  36290  copsex2d  37453  finxpreclem3  37709  eqrelf  38579  dvnprodlem1  46374  or2expropbilem1  47480  or2expropbilem2  47481  funop1  47731  ich2exprop  47931  ichnreuop  47932  ichreuopeq  47933  reuopreuprim  47986  uspgrsprf1  48623