Theorem nfs1v 2152

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

Syntax hints:   → wi 4  ∀wal 1535  Ⅎwnf 1781  [wsb 2064

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-10 2136

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-ex 1778  df-nf 1782  df-sb 2065

This theorem is referenced by:  hbs1  2269  sb5OLD  2272  sb8fOLD  2353  sb8ef  2354  sbbib  2360  sb2ae  2498  mo3  2561  eu1  2607  2mo  2645  2eu6  2654  nfsab1  2719  cbvrexsvw  3319  cbvralsvwOLD  3320  cbvralsvwOLDOLD  3321  cbvrexsvwOLD  3322  cbvralf  3363  cbvralsv  3369  cbvrexsv  3370  cbvrabwOLD  3476  cbvrab  3481  sbhypfOLD  3552  mob2  3731  reu2  3741  reu2eqd  3752  sbcralt  3888  sbcreu  3892  cbvrabcsfw  3959  cbvreucsf  3962  cbvrabcsf  3963  sbcel12  4430  sbceqg  4431  2nreu  4463  csbif  4605  rexreusng  4703  cbvopab1  5244  cbvopab1g  5245  cbvopab1s  5247  cbvmptf  5278  cbvmptfg  5279  csbopab  5578  csbopabgALT  5579  opeliunxp  5766  ralxpf  5870  cbviotaw  6531  cbviota  6534  csbiota  6565  isarep1  6666  isarep1OLD  6667  f1ossf1o  7160  cbvriotaw  7410  cbvriota  7415  csbriota  7417  onminex  7834  tfis  7888  findes  7936  abrexex2g  8001  dfoprab4f  8093  axrepndlem1  10657  axrepndlem2  10658  uzind4s  12969  mo5f  32508  ac6sf2  32635  esumcvg  34042  bj-gabima  36854  wl-lem-moexsb  37470  wl-mo3t  37478  poimirlem26  37554  sbcalf  38022  sbcexf  38023  sbcrexgOLD  42678  scottabes  44151  2sb5nd  44471  2sb5ndALT  44843  2reu8i  46960  dfich2  47264  opeliun2xp  47975