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

Theorem mpoeq3ia 7289
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 1132 . . 3 ((⊤ ∧ 𝑥𝐴𝑦𝐵) → 𝐶 = 𝐷)
32mpoeq3dva 7288 . 2 (⊤ → (𝑥𝐴, 𝑦𝐵𝐶) = (𝑥𝐴, 𝑦𝐵𝐷))
43mptru 1550 1 (𝑥𝐴, 𝑦𝐵𝐶) = (𝑥𝐴, 𝑦𝐵𝐷)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399   = wceq 1543  wtru 1544  wcel 2110  cmpo 7215
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-9 2120  ax-12 2175  ax-ext 2708
This theorem depends on definitions:  df-bi 210  df-an 400  df-3an 1091  df-tru 1546  df-ex 1788  df-nf 1792  df-sb 2071  df-clab 2715  df-cleq 2729  df-oprab 7217  df-mpo 7218
This theorem is referenced by:  mpodifsnif  7325  mposnif  7326  oprab2co  7865  cnfcomlem  9314  cnfcom2  9317  dfioo2  13038  elovmpowrd  14113  sadcom  16022  comfffval2  17204  oppchomf  17224  symgga  18799  oppglsm  19031  dfrhm2  19737  cnfldsub  20391  cnflddiv  20393  mat0op  21316  mattpos1  21353  mdetunilem7  21515  madufval  21534  maducoeval2  21537  madugsum  21540  mp2pm2mplem5  21707  mp2pm2mp  21708  leordtval  22110  xpstopnlem1  22706  divcn  23765  oprpiece1res1  23848  oprpiece1res2  23849  ehl1eudis  24317  ehl2eudis  24319  cxpcn  25631  cnnvm  28763  mdetpmtr2  31488  madjusmdetlem1  31491  cnre2csqima  31575  mndpluscn  31590  raddcn  31593  icorempo  35259  matunitlindflem1  35510  mendplusgfval  40713  hoidmv1le  43807  hspdifhsp  43829  vonn0ioo  43900  vonn0icc  43901  dflinc2  45424
  Copyright terms: Public domain W3C validator