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

Theorem nfs1v 2313
Description: The setvar 𝑥 is not free in [𝑦 / 𝑥]𝜑 when 𝑥 and 𝑦 are distinct. (Contributed by Mario Carneiro, 11-Aug-2016.) Shorten nfs1v and hbs1 2314 combined. (Revised by Wolf Lammen, 28-Jul-2022.)
Assertion
Ref Expression
nfs1v 𝑥[𝑦 / 𝑥]𝜑
Distinct variable group:   𝑥,𝑦
Allowed substitution hints:   𝜑(𝑥,𝑦)

Proof of Theorem nfs1v
StepHypRef Expression
1 sb6 2309 . 2 ([𝑦 / 𝑥]𝜑 ↔ ∀𝑥(𝑥 = 𝑦𝜑))
2 nfa1 2204 . 2 𝑥𝑥(𝑥 = 𝑦𝜑)
31, 2nfxfr 1954 1 𝑥[𝑦 / 𝑥]𝜑
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1656  wnf 1884  [wsb 2069
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-10 2194  ax-12 2222
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 881  df-ex 1881  df-nf 1885  df-sb 2070
This theorem is referenced by:  hbs1  2314  sb8v  2378  sb8ev  2379  mo3  2633  mo3OLD  2634  eu1  2695  eu1OLD  2696  2mo  2731  2eu6  2738  cbvralf  3377  cbvralsv  3394  cbvrexsv  3395  cbvrab  3411  sbhypf  3470  mob2  3611  reu2  3619  reu2eqd  3630  sbcralt  3735  sbcreu  3739  cbvreucsf  3791  cbvrabcsf  3792  sbcel12  4207  sbceqg  4208  csbif  4361  cbvopab1  4946  cbvopab1s  4948  cbvmptf  4971  cbvmpt  4972  opelopabsb  5211  csbopab  5234  csbopabgALT  5235  opeliunxp  5403  ralxpf  5501  cbviota  6091  csbiota  6116  isarep1  6210  f1ossf1o  6645  cbvriota  6876  csbriota  6878  onminex  7268  tfis  7315  findes  7357  abrexex2g  7405  dfoprab4f  7488  axrepndlem1  9729  axrepndlem2  9730  uzind4s  12030  mo5f  29879  ac6sf2  29978  esumcvg  30693  bj-mo3OLD  33356  wl-lem-moexsb  33894  wl-mo3t  33902  poimirlem26  33979  sbcalf  34458  sbcexf  34459  sbcrexgOLD  38193  2sb5nd  39604  2sb5ndALT  39986  opeliun2xp  42958
  Copyright terms: Public domain W3C validator