Theorem opeq12 4879

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1536  ⟨cop 4636

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637

This theorem is referenced by:  opeq12i  4882  opeq12d  4885  cbvopab  5219  cbvopabv  5220  opth  5486  copsex2t  5502  relop  5863  funopg  6601  fvn0ssdmfun  7093  fsn  7154  fnressn  7177  fmptsng  7187  fmptsnd  7188  tpres  7220  cbvoprab12  7521  cbvoprab12v  7522  eqopi  8048  f1o2ndf1  8145  tposoprab  8285  omeu  8621  brecop  8848  ecovcom  8861  ecovass  8862  ecovdi  8863  xpf1o  9177  addsrmo  11110  mulsrmo  11111  addsrpr  11112  mulsrpr  11113  addcnsr  11172  axcnre  11201  seqeq1  14041  opfi1uzind  14546  fsumcnv  15805  fprodcnv  16015  eucalgval2  16614  xpstopnlem1  23832  qustgplem  24144  finsumvtxdg2size  29582  brabgaf  32627  qqhval2  33944  brsegle  36089  copsex2d  37121  finxpreclem3  37375  eqrelf  38236  dvnprodlem1  45901  or2expropbilem1  46981  or2expropbilem2  46982  funop1  47232  ich2exprop  47395  ichnreuop  47396  ichreuopeq  47397  reuopreuprim  47450  uspgrsprf1  47990