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

Theorem mpt2eq3ia 6877
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 1124 . . 3 ((⊤ ∧ 𝑥𝐴𝑦𝐵) → 𝐶 = 𝐷)
32mpt2eq3dva 6876 . 2 (⊤ → (𝑥𝐴, 𝑦𝐵𝐶) = (𝑥𝐴, 𝑦𝐵𝐷))
43trud 1634 1 (𝑥𝐴, 𝑦𝐵𝐶) = (𝑥𝐴, 𝑦𝐵𝐷)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383   = wceq 1624  wtru 1625  wcel 2131  cmpt2 6807
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1863  ax-4 1878  ax-5 1980  ax-6 2046  ax-7 2082  ax-9 2140  ax-10 2160  ax-11 2175  ax-12 2188  ax-13 2383  ax-ext 2732
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1627  df-ex 1846  df-nf 1851  df-sb 2039  df-clab 2739  df-cleq 2745  df-clel 2748  df-oprab 6809  df-mpt2 6810
This theorem is referenced by:  mpt2difsnif  6910  mpt2snif  6911  oprab2co  7422  cnfcomlem  8761  cnfcom2  8764  dfioo2  12459  elovmpt2wrd  13526  sadcom  15379  comfffval2  16554  oppchomf  16573  symgga  18018  oppglsm  18249  dfrhm2  18911  cnfldsub  19968  cnflddiv  19970  mat0op  20419  mattpos1  20456  mdetunilem7  20618  madufval  20637  maducoeval2  20640  madugsum  20643  mp2pm2mplem5  20809  mp2pm2mp  20810  leordtval  21211  xpstopnlem1  21806  divcn  22864  oprpiece1res1  22943  oprpiece1res2  22944  cxpcn  24677  cnnvm  27838  mdetpmtr2  30191  madjusmdetlem1  30194  cnre2csqima  30258  mndpluscn  30273  raddcn  30276  icorempt2  33502  matunitlindflem1  33710  mendplusgfval  38249  hoidmv1le  41306  hspdifhsp  41328  vonn0ioo  41399  vonn0icc  41400  dflinc2  42701
  Copyright terms: Public domain W3C validator