Theorem opeq12 4842

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

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

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 2148  ax-9 2156  ax-ext 2737

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 2744  df-cleq 2757  df-clel 2840  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598

This theorem is used by:  opeq12i  4845  opeq12d  4848  cbvopab  5185  cbvopabv  5186  opth  5460  copsex2t  5477  relop  5838  funopg  6574  fvn0ssdmfun  7073  fsn  7135  fnressn  7161  fmptsng  7172  fmptsnd  7173  tpres  7206  cbvoprab12  7508  cbvoprab12v  7509  eqopi  8028  f1o2ndf1  8123  tposoprab  8264  omeu  8576  brecop  8814  ecovcom  8827  ecovass  8828  ecovdi  8829  xpf1o  9134  addsrmo  11073  mulsrmo  11074  addsrpr  11075  mulsrpr  11076  addcnsr  11135  axcnre  11164  seqeq1  14058  opfi1uzind  14566  fsumcnv  15847  fprodcnv  16060  eucalgval2  16661  degenmgm2nfun  19039  xpstopnlem1  24017  qustgplem  24329  finsumvtxdg2size  29958  brabgaf  33022  qqhval2  34436  brsegle  36637  copsex2d  37840  finxpreclem3  38096  eqrelf  38965  dvnprodlem1  46718  or2expropbilem1  47827  or2expropbilem2  47828  funop1  48078  ich2exprop  48278  ichnreuop  48279  ichreuopeq  48280  reuopreuprim  48333  uspgrsprf1  48970