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

Theorem nfs1v 2436
Description: The setvar 𝑥 is not free in [𝑦 / 𝑥]𝜑 when 𝑥 and 𝑦 are distinct. (Contributed by Mario Carneiro, 11-Aug-2016.)
Assertion
Ref Expression
nfs1v 𝑥[𝑦 / 𝑥]𝜑
Distinct variable group:   𝑥,𝑦
Allowed substitution hints:   𝜑(𝑥,𝑦)

Proof of Theorem nfs1v
StepHypRef Expression
1 hbs1 2435 . 2 ([𝑦 / 𝑥]𝜑 → ∀𝑥[𝑦 / 𝑥]𝜑)
21nf5i 2021 1 𝑥[𝑦 / 𝑥]𝜑
Colors of variables: wff setvar class
Syntax hints:  wnf 1705  [wsb 1877
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-10 2016  ax-12 2044  ax-13 2245
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-ex 1702  df-nf 1707  df-sb 1878
This theorem is referenced by:  mo3  2506  eu1  2509  2mo  2550  2eu6  2557  cbvralf  3156  cbvralsv  3173  cbvrexsv  3174  cbvrab  3187  sbhypf  3242  mob2  3372  reu2  3380  reu2eqd  3389  sbcralt  3496  sbcreu  3501  cbvreucsf  3552  cbvrabcsf  3553  sbcel12  3960  sbceqg  3961  csbif  4115  rabasiun  4494  cbvopab1  4690  cbvopab1s  4692  cbvmptf  4713  cbvmpt  4714  opelopabsb  4950  csbopab  4973  csbopabgALT  4974  opeliunxp  5136  ralxpf  5233  cbviota  5820  csbiota  5845  isarep1  5940  cbvriota  6581  csbriota  6583  onminex  6961  tfis  7008  findes  7050  abrexex2g  7097  abrexex2  7101  dfoprab4f  7178  axrepndlem1  9366  axrepndlem2  9367  uzind4s  11700  mo5f  29195  ac6sf2  29295  esumcvg  29953  bj-mo3OLD  32512  wl-lem-moexsb  33017  wl-mo3t  33025  poimirlem26  33102  sbcalf  33584  sbcexf  33585  sbcrexgOLD  36864  sbcel12gOLD  38271  2sb5nd  38293  2sb5ndALT  38686  opeliun2xp  41425
  Copyright terms: Public domain W3C validator