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 2815	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 2732

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 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  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  5452  copsex2t  5469  relop  5830  funopg  6567  fvn0ssdmfun  7067  fsn  7129  fnressn  7155  fmptsng  7166  fmptsnd  7167  tpres  7200  cbvoprab12  7502  cbvoprab12v  7503  eqopi  8022  f1o2ndf1  8119  tposoprab  8260  omeu  8572  brecop  8810  ecovcom  8823  ecovass  8824  ecovdi  8825  xpf1o  9137  addsrmo  11082  mulsrmo  11083  addsrpr  11084  mulsrpr  11085  addcnsr  11144  axcnre  11173  seqeq1  14068  opfi1uzind  14576  fsumcnv  15859  fprodcnv  16070  eucalgval2  16671  degenmgm2nfun  19052  xpstopnlem1  24035  qustgplem  24347  finsumvtxdg2size  30010  brabgaf  33079  qqhval2  34492  brsegle  36688  copsex2d  37891  finxpreclem3  38147  eqrelf  39006  dvnprodlem1  46774  or2expropbilem1  47920  or2expropbilem2  47921  funop1  48171  ich2exprop  48371  ichnreuop  48372  ichreuopeq  48373  reuopreuprim  48426  uspgrsprf1  49063