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

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

Proof of Theorem mpoeq3ia
StepHypRef Expression
1 mpoeq3ia.1 . . . 4 ((𝑥𝐴𝑦𝐵) → 𝐶 = 𝐷)
213adant1 1131 . . 3 ((⊤ ∧ 𝑥𝐴𝑦𝐵) → 𝐶 = 𝐷)
32mpoeq3dva 7510 . 2 (⊤ → (𝑥𝐴, 𝑦𝐵𝐶) = (𝑥𝐴, 𝑦𝐵𝐷))
43mptru 1547 1 (𝑥𝐴, 𝑦𝐵𝐶) = (𝑥𝐴, 𝑦𝐵𝐷)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395   = wceq 1540  wtru 1541  wcel 2108  cmpo 7433
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1089  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-oprab 7435  df-mpo 7436
This theorem is referenced by:  mpodifsnif  7548  mposnif  7549  oprab2co  8122  cnfcomlem  9739  cnfcom2  9742  dfioo2  13490  elovmpowrd  14596  sadcom  16500  comfffval2  17744  oppchomf  17763  symgga  19425  oppglsm  19660  dfrhm2  20474  cnfldsub  21410  cnflddiv  21413  cnflddivOLD  21414  mat0op  22425  mattpos1  22462  mdetunilem7  22624  madufval  22643  maducoeval2  22646  madugsum  22649  mp2pm2mplem5  22816  mp2pm2mp  22817  leordtval  23221  xpstopnlem1  23817  divcnOLD  24890  divcn  24892  oprpiece1res1  24982  oprpiece1res2  24983  ehl1eudis  25454  ehl2eudis  25456  cxpcn  26787  cxpcnOLD  26788  cnnvm  30701  mdetpmtr2  33823  madjusmdetlem1  33826  cnre2csqima  33910  mndpluscn  33925  raddcn  33928  icorempo  37352  matunitlindflem1  37623  mendplusgfval  43193  hoidmv1le  46609  hspdifhsp  46631  vonn0ioo  46702  vonn0icc  46703  dflinc2  48327  dfswapf2  48967
  Copyright terms: Public domain W3C validator