Theorem nfs1v 2157

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

Syntax hints:   → wi 4  ∀wal 1538  Ⅎwnf 1783  [wsb 2065

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 1967  ax-7 2008  ax-10 2142

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1780  df-nf 1784  df-sb 2066

This theorem is referenced by:  hbs1  2274  sb8ef  2353  sbbib  2359  sb2ae  2494  mo3  2557  eu1  2603  2mo  2641  2eu6  2650  nfsab1  2715  cbvrexsvw  3288  cbvralsvwOLD  3289  cbvralsvwOLDOLD  3290  cbvrexsvwOLD  3291  cbvralf  3331  cbvralsv  3337  cbvrexsv  3338  cbvrabwOLD  3439  cbvrab  3443  sbhypfOLD  3508  mob2  3683  reu2  3693  reu2eqd  3704  sbcralt  3832  sbcreu  3836  cbvrabcsfw  3900  cbvreucsf  3903  cbvrabcsf  3904  sbcel12  4370  sbceqg  4371  2nreu  4403  csbif  4542  rexreusng  4639  cbvopab1  5176  cbvopab1g  5177  cbvopab1s  5179  cbvmptf  5202  cbvmptfg  5203  csbopab  5510  csbopabgALT  5511  opeliunxp  5698  opeliun2xp  5699  ralxpf  5800  cbviotaw  6459  cbviota  6461  csbiota  6492  isarep1  6589  f1ossf1o  7082  cbvriotaw  7335  cbvriota  7339  csbriota  7341  onminex  7758  tfis  7811  findes  7856  abrexex2g  7922  dfoprab4f  8014  axrepndlem1  10521  axrepndlem2  10522  uzind4s  12843  mo5f  32468  ac6sf2  32598  esumcvg  34069  bj-gabima  36921  wl-lem-moexsb  37549  wl-mo3t  37557  poimirlem26  37633  sbcalf  38101  sbcexf  38102  sbcrexgOLD  42766  scottabes  44224  2sb5nd  44543  2sb5ndALT  44914  2reu8i  47107  dfich2  47452