MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mpt2eq3ia Structured version   Visualization version   GIF version

Theorem mpt2eq3ia 6618
Description: An equality inference for the maps to notation. (Contributed by Mario Carneiro, 16-Dec-2013.)
Hypothesis
Ref Expression
mpt2eq3ia.1 ((𝑥𝐴𝑦𝐵) → 𝐶 = 𝐷)
Assertion
Ref Expression
mpt2eq3ia (𝑥𝐴, 𝑦𝐵𝐶) = (𝑥𝐴, 𝑦𝐵𝐷)

Proof of Theorem mpt2eq3ia
StepHypRef Expression
1 mpt2eq3ia.1 . . . 4 ((𝑥𝐴𝑦𝐵) → 𝐶 = 𝐷)
213adant1 1072 . . 3 ((⊤ ∧ 𝑥𝐴𝑦𝐵) → 𝐶 = 𝐷)
32mpt2eq3dva 6617 . 2 (⊤ → (𝑥𝐴, 𝑦𝐵𝐶) = (𝑥𝐴, 𝑦𝐵𝐷))
43trud 1484 1 (𝑥𝐴, 𝑦𝐵𝐶) = (𝑥𝐴, 𝑦𝐵𝐷)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383   = wceq 1475  wtru 1476  wcel 1977  cmpt2 6551
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-oprab 6553  df-mpt2 6554
This theorem is referenced by:  mpt2difsnif  6651  mpt2snif  6652  oprab2co  7149  cnfcomlem  8479  cnfcom2  8482  dfioo2  12145  elovmpt2wrd  13202  sadcom  15023  comfffval2  16184  oppchomf  16203  symgga  17649  oppglsm  17880  dfrhm2  18540  cnfldsub  19593  cnflddiv  19595  mat0op  20044  mattpos1  20081  mdetunilem7  20243  madufval  20262  maducoeval2  20265  madugsum  20268  mp2pm2mplem5  20434  mp2pm2mp  20435  leordtval  20827  xpstopnlem1  21422  divcn  22479  oprpiece1res1  22558  oprpiece1res2  22559  cxpcn  24286  wwlknprop  26214  numclwwlk5  26639  numclwwlk7  26641  cnnvm  26921  mdetpmtr2  29218  madjusmdetlem1  29221  cnre2csqima  29285  mndpluscn  29300  raddcn  29303  icorempt2  32375  matunitlindflem1  32575  mendplusgfval  36774  hoidmv1le  39484  hspdifhsp  39506  vonn0ioo  39578  vonn0icc  39579  av-numclwwlk5  41542  av-numclwwlk6  41544  dflinc2  41993
  Copyright terms: Public domain W3C validator