Theorem opeq12 4841

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-ss 3897  df-dif 4046  df-un 4150  df-nul 4278  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835

This theorem is used by:  opeq12i  4844  opeq12d  4847  cbvopab  5176  cbvopabv  5177  opth  5445  copsex2t  5464  relop  5829  funopg  6579  fvn0ssdmfun  7079  fsn  7141  fnressn  7167  fmptsng  7177  fmptsnd  7178  tpres  7211  cbvoprab12  7513  cbvoprab12v  7514  eqopi  8041  f1o2ndf1  8139  tposoprab  8286  omeu  8600  brecop  8838  ecovcom  8851  ecovass  8852  ecovdi  8853  xpf1o  9165  addsrmo  11165  mulsrmo  11166  addsrpr  11167  mulsrpr  11168  addcnsr  11227  axcnre  11256  seqeq1  14154  opfi1uzind  14663  fsumcnv  15948  fprodcnv  16159  eucalgval2  16765  degenmgm2nfun  19148  xpstopnlem1  24137  qustgplem  24449  finsumvtxdg2size  30140  brabgaf  33251  qqhval2  34664  brsegle  36969  copsex2d  38169  finxpreclem3  38425  eqrelf  39299  dvnprodlem1  47064  or2expropbilem1  48210  or2expropbilem2  48211  funop1  48461  ich2exprop  48661  ichnreuop  48662  ichreuopeq  48663  reuopreuprim  48716  uspgrsprf1  49353