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

Theorem nfs1v 2159
Description: The setvar 𝑥 is not free in [𝑦 / 𝑥]𝜑 when 𝑥 and 𝑦 are distinct. (Contributed by Mario Carneiro, 11-Aug-2016.) Shorten nfs1v 2159 and hbs1 2273 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 2092 . 2 ([𝑦 / 𝑥]𝜑 ↔ ∀𝑥(𝑥 = 𝑦𝜑))
2 nfa1 2154 . 2 𝑥𝑥(𝑥 = 𝑦𝜑)
31, 2nfxfr 1852 1 𝑥[𝑦 / 𝑥]𝜑
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1534  wnf 1783  [wsb 2068
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1969  ax-7 2014  ax-10 2144
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-ex 1780  df-nf 1784  df-sb 2069
This theorem is referenced by:  hbs1  2273  sb5  2275  sbbibOLD  2288  sb8v  2372  sb8ev  2373  sbbib  2379  sb2ae  2535  mo3  2647  eu1  2693  2mo  2732  2eu6  2743  nfsab1  2811  cbvralfw  3440  cbvralf  3442  cbvralsvw  3470  cbvrexsvw  3471  cbvralsv  3472  cbvrexsv  3473  cbvrabw  3492  cbvrab  3493  sbhypf  3555  mob2  3709  reu2  3719  reu2eqd  3730  sbcralt  3858  sbcreu  3862  cbvrabcsfw  3927  cbvreucsf  3930  cbvrabcsf  3931  sbcel12  4363  sbceqg  4364  2nreu  4396  csbif  4525  rexreusng  4620  cbvopab1  5142  cbvopab1g  5143  cbvopab1s  5145  cbvmptf  5168  cbvmptfg  5169  opelopabsb  5420  csbopab  5445  csbopabgALT  5446  opeliunxp  5622  ralxpf  5720  cbviotaw  6324  cbviota  6326  csbiota  6351  isarep1  6445  f1ossf1o  6893  cbvriotaw  7126  cbvriota  7130  csbriota  7132  onminex  7525  tfis  7572  findes  7615  abrexex2g  7668  dfoprab4f  7757  axrepndlem1  10017  axrepndlem2  10018  uzind4s  12311  mo5f  30256  ac6sf2  30373  esumcvg  31349  wl-lem-moexsb  34808  wl-mo3t  34816  poimirlem26  34922  sbcalf  35396  sbcexf  35397  sbcrexgOLD  39388  scottabes  40584  2sb5nd  40900  2sb5ndALT  41272  2reu8i  43319  dfich2  43620  dfich2ai  43621  dfich2OLD  43623  ichnfimlem2  43629  opeliun2xp  44388
  Copyright terms: Public domain W3C validator