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

Theorem mpt2eq3ia 6883
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 1125 . . 3 ((⊤ ∧ 𝑥𝐴𝑦𝐵) → 𝐶 = 𝐷)
32mpt2eq3dva 6882 . 2 (⊤ → (𝑥𝐴, 𝑦𝐵𝐶) = (𝑥𝐴, 𝑦𝐵𝐷))
43trud 1640 1 (𝑥𝐴, 𝑦𝐵𝐶) = (𝑥𝐴, 𝑦𝐵𝐷)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383   = wceq 1630  wtru 1631  wcel 2137  cmpt2 6813
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1986  ax-6 2052  ax-7 2088  ax-9 2146  ax-10 2166  ax-11 2181  ax-12 2194  ax-13 2389  ax-ext 2738
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2045  df-clab 2745  df-cleq 2751  df-clel 2754  df-oprab 6815  df-mpt2 6816
This theorem is referenced by:  mpt2difsnif  6916  mpt2snif  6917  oprab2co  7428  cnfcomlem  8767  cnfcom2  8770  dfioo2  12465  elovmpt2wrd  13532  sadcom  15385  comfffval2  16560  oppchomf  16579  symgga  18024  oppglsm  18255  dfrhm2  18917  cnfldsub  19974  cnflddiv  19976  mat0op  20425  mattpos1  20462  mdetunilem7  20624  madufval  20643  maducoeval2  20646  madugsum  20649  mp2pm2mplem5  20815  mp2pm2mp  20816  leordtval  21217  xpstopnlem1  21812  divcn  22870  oprpiece1res1  22949  oprpiece1res2  22950  cxpcn  24683  cnnvm  27844  mdetpmtr2  30197  madjusmdetlem1  30200  cnre2csqima  30264  mndpluscn  30279  raddcn  30282  icorempt2  33508  matunitlindflem1  33716  mendplusgfval  38255  hoidmv1le  41312  hspdifhsp  41334  vonn0ioo  41405  vonn0icc  41406  dflinc2  42707
  Copyright terms: Public domain W3C validator