Theorem nfs1v 2161

Description: The setvar 𝑥 is not free in [𝑦 / 𝑥]𝜑 when 𝑥 and 𝑦 are distinct. (Contributed by Mario Carneiro, 11-Aug-2016.) Shorten nfs1v 2161 and hbs1 2274 combined. (Revised by Wolf Lammen, 28-Jul-2022.)

Assertion

Ref	Expression
nfs1v	⊢ Ⅎ𝑥[𝑦 / 𝑥]𝜑

Distinct variable group:   𝑥,𝑦

Allowed substitution hints:   𝜑(𝑥,𝑦)

Proof of Theorem nfs1v

Step	Hyp	Ref	Expression
1		sb6 2095	. 2 ⊢ ([𝑦 / 𝑥]𝜑 ↔ ∀𝑥(𝑥 = 𝑦 → 𝜑))
2		nfa1 2156	. 2 ⊢ Ⅎ𝑥∀𝑥(𝑥 = 𝑦 → 𝜑)
3	1, 2	nfxfr 1859	1 ⊢ Ⅎ𝑥[𝑦 / 𝑥]𝜑

Syntax hints:   → wi 4  ∀wal 1540  Ⅎwnf 1790  [wsb 2074

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-10 2145

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-ex 1787  df-nf 1791  df-sb 2075

This theorem is referenced by:  hbs1  2274  sb5OLD  2277  sb8v  2356  sb8ev  2357  sbbib  2363  sb2ae  2501  mo3  2565  eu1  2614  2mo  2652  2eu6  2660  nfsab1  2726  cbvralfwOLD  3337  cbvralf  3339  cbvralsvw  3369  cbvrexsvw  3370  cbvralsv  3371  cbvrexsv  3372  cbvrabw  3392  cbvrab  3393  sbhypf  3459  mob2  3619  reu2  3629  reu2eqd  3640  sbcralt  3773  sbcreu  3777  cbvrabcsfw  3841  cbvreucsf  3844  cbvrabcsf  3845  sbcel12  4308  sbceqg  4309  2nreu  4341  csbif  4481  rexreusng  4580  cbvopab1  5113  cbvopab1g  5114  cbvopab1s  5116  cbvmptf  5139  cbvmptfg  5140  csbopab  5420  csbopabgALT  5421  opeliunxp  5600  ralxpf  5699  cbviotaw  6314  cbviota  6317  csbiota  6342  isarep1  6437  f1ossf1o  6912  cbvriotaw  7148  cbvriota  7153  csbriota  7155  onminex  7553  tfis  7600  findes  7645  abrexex2g  7702  dfoprab4f  7791  axrepndlem1  10104  axrepndlem2  10105  uzind4s  12402  mo5f  30423  ac6sf2  30546  esumcvg  31636  bj-gabima  34783  wl-lem-moexsb  35378  wl-mo3t  35386  poimirlem26  35458  sbcalf  35927  sbcexf  35928  sbcrexgOLD  40219  scottabes  41442  2sb5nd  41758  2sb5ndALT  42130  2reu8i  44185  dfich2  44491  opeliun2xp  45249