Theorem nfs1v 2155

Description: The setvar 𝑥 is not free in [𝑦 / 𝑥]𝜑 when 𝑥 and 𝑦 are distinct. (Contributed by Mario Carneiro, 11-Aug-2016.) Shorten nfs1v 2155 and hbs1 2269 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 2089	. 2 ⊢ ([𝑦 / 𝑥]𝜑 ↔ ∀𝑥(𝑥 = 𝑦 → 𝜑))
2		nfa1 2150	. 2 ⊢ Ⅎ𝑥∀𝑥(𝑥 = 𝑦 → 𝜑)
3	1, 2	nfxfr 1856	1 ⊢ Ⅎ𝑥[𝑦 / 𝑥]𝜑

Syntax hints:   → wi 4  ∀wal 1537  Ⅎwnf 1787  [wsb 2068

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-10 2139

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-ex 1784  df-nf 1788  df-sb 2069

This theorem is referenced by:  hbs1  2269  sb5OLD  2272  sb8v  2352  sb8ev  2353  sbbib  2359  sb2ae  2500  mo3  2564  eu1  2612  2mo  2650  2eu6  2658  nfsab1  2723  cbvralfwOLD  3359  cbvralf  3361  cbvralsvw  3391  cbvrexsvw  3392  cbvralsv  3393  cbvrexsv  3394  cbvrabw  3414  cbvrab  3415  sbhypf  3481  mob2  3645  reu2  3655  reu2eqd  3666  sbcralt  3801  sbcreu  3805  cbvrabcsfw  3872  cbvreucsf  3875  cbvrabcsf  3876  sbcel12  4339  sbceqg  4340  2nreu  4372  csbif  4513  rexreusng  4612  cbvopab1  5145  cbvopab1g  5146  cbvopab1s  5148  cbvmptf  5179  cbvmptfg  5180  csbopab  5461  csbopabgALT  5462  opeliunxp  5645  ralxpf  5744  cbviotaw  6383  cbviota  6386  csbiota  6411  isarep1  6506  f1ossf1o  6982  cbvriotaw  7221  cbvriota  7226  csbriota  7228  onminex  7629  tfis  7676  findes  7723  abrexex2g  7780  dfoprab4f  7869  axrepndlem1  10279  axrepndlem2  10280  uzind4s  12577  mo5f  30738  ac6sf2  30861  esumcvg  31954  bj-gabima  35055  wl-lem-moexsb  35650  wl-mo3t  35658  poimirlem26  35730  sbcalf  36199  sbcexf  36200  sbcrexgOLD  40523  scottabes  41749  2sb5nd  42069  2sb5ndALT  42441  2reu8i  44492  dfich2  44798  opeliun2xp  45556