ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  mpteq2dv GIF version

Theorem mpteq2dv 3977
Description: An equality inference for the maps-to notation. (Contributed by Mario Carneiro, 23-Aug-2014.)
Hypothesis
Ref Expression
mpteq2dv.1 (𝜑𝐵 = 𝐶)
Assertion
Ref Expression
mpteq2dv (𝜑 → (𝑥𝐴𝐵) = (𝑥𝐴𝐶))
Distinct variable group:   𝜑,𝑥
Allowed substitution hints:   𝐴(𝑥)   𝐵(𝑥)   𝐶(𝑥)

Proof of Theorem mpteq2dv
StepHypRef Expression
1 mpteq2dv.1 . . 3 (𝜑𝐵 = 𝐶)
21adantr 272 . 2 ((𝜑𝑥𝐴) → 𝐵 = 𝐶)
32mpteq2dva 3976 1 (𝜑 → (𝑥𝐴𝐵) = (𝑥𝐴𝐶))
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1312  wcel 1461  cmpt 3947
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1404  ax-7 1405  ax-gen 1406  ax-ie1 1450  ax-ie2 1451  ax-8 1463  ax-11 1465  ax-4 1468  ax-17 1487  ax-i9 1491  ax-ial 1495  ax-i5r 1496  ax-ext 2095
This theorem depends on definitions:  df-bi 116  df-tru 1315  df-nf 1418  df-sb 1717  df-clab 2100  df-cleq 2106  df-clel 2109  df-ral 2393  df-opab 3948  df-mpt 3949
This theorem is referenced by:  ofeq  5936  rdgeq1  6219  rdgeq2  6220  omv  6302  oeiv  6303  0tonninf  10098  1tonninf  10099  iseqf1olemjpcl  10154  iseqf1olemqpcl  10155  iseqf1olemfvp  10156  seq3f1olemqsum  10159  seq3f1olemp  10161  summodc  11037  zsumdc  11038  fsum3  11041  sloteq  11800  cnprcl2k  12210  fsumcncntop  12535  expcncf  12571  peano4nninf  12877  peano3nninf  12878  nninfalllem1  12880  nninfsellemdc  12883  nninfsellemeq  12887  nninfsellemqall  12888  nninfsellemeqinf  12889  nninfomni  12892
  Copyright terms: Public domain W3C validator