Theorem opeq12 4847

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

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

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

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 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4841

This theorem is used by:  opeq12i  4850  opeq12d  4853  cbvopab  5183  cbvopabv  5184  opth  5452  copsex2t  5471  relopabi  5809  relop  5838  funopg  6602  fvn0ssdmfun  7106  fsn  7168  fnressn  7194  fmptsng  7204  fmptsnd  7205  tpres  7238  cbvoprab12  7540  cbvoprab12v  7541  eqopi  8071  f1o2ndf1  8170  tposoprab  8317  omeu  8631  brecop  8869  ecovcom  8882  ecovass  8883  ecovdi  8884  xpf1o  9196  addsrmo  11197  mulsrmo  11198  addsrpr  11199  mulsrpr  11200  addcnsr  11259  axcnre  11288  seqeq1  14187  opfi1uzind  14697  fsumcnv  15983  fprodcnv  16194  eucalgval2  16800  degenmgm2nfun  19189  xpstopnlem1  24183  qustgplem  24495  finsumvtxdg2size  30188  brabgaf  33298  qqhval2  34725  brsegle  37088  copsex2d  38331  finxpreclem3  38584  eqrelf  39456  dvnprodlem1  47229  or2expropbilem1  48375  or2expropbilem2  48376  funop1  48626  ich2exprop  48826  ichnreuop  48827  ichreuopeq  48828  reuopreuprim  48881  uspgrsprf1  49518