Theorem opeq12 4835

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570  ⟨cop 4590

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591

This theorem is used by:  opeq12i  4838  opeq12d  4841  cbvopab  5177  cbvopabv  5178  opth  5445  copsex2t  5464  relop  5828  funopg  6572  fvn0ssdmfun  7072  fsn  7134  fnressn  7160  fmptsng  7171  fmptsnd  7172  tpres  7205  cbvoprab12  7507  cbvoprab12v  7508  eqopi  8035  f1o2ndf1  8131  tposoprab  8272  omeu  8586  brecop  8824  ecovcom  8837  ecovass  8838  ecovdi  8839  xpf1o  9151  addsrmo  11151  mulsrmo  11152  addsrpr  11153  mulsrpr  11154  addcnsr  11213  axcnre  11242  seqeq1  14140  opfi1uzind  14649  fsumcnv  15932  fprodcnv  16143  eucalgval2  16749  degenmgm2nfun  19132  xpstopnlem1  24121  qustgplem  24433  finsumvtxdg2size  30124  brabgaf  33193  qqhval2  34607  brsegle  36853  copsex2d  38040  finxpreclem3  38296  eqrelf  39170  dvnprodlem1  46925  or2expropbilem1  48071  or2expropbilem2  48072  funop1  48322  ich2exprop  48522  ichnreuop  48523  ichreuopeq  48524  reuopreuprim  48577  uspgrsprf1  49214