Theorem nfs1v 2162

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

Syntax hints:   → wi 4  ∀wal 1540  Ⅎwnf 1785  [wsb 2068

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-10 2147

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-ex 1782  df-nf 1786  df-sb 2069

This theorem is referenced by:  hbs1  2281  sb8ef  2360  sbbib  2366  sb2ae  2501  mo3  2565  eu1  2611  2mo  2649  2eu6  2658  nfsab1  2723  cbvrexsvw  3290  cbvralsvwOLD  3291  cbvralf  3323  cbvralsv  3329  cbvrexsv  3330  cbvrabwOLD  3426  cbvrab  3429  mob2  3662  reu2  3672  reu2eqd  3683  sbcralt  3811  sbcreu  3815  cbvrabcsfw  3879  cbvreucsf  3882  cbvrabcsf  3883  sbcel12  4352  sbceqg  4353  2nreu  4385  csbif  4525  rexreusng  4624  cbvopab1  5160  cbvopab1g  5161  cbvopab1s  5163  cbvmptf  5186  cbvmptfg  5187  csbopab  5505  csbopabgALT  5506  opeliunxp  5693  opeliun2xp  5694  ralxpf  5797  cbviotaw  6457  cbviota  6459  csbiota  6487  isarep1  6583  f1ossf1o  7077  cbvriotaw  7328  cbvriota  7332  csbriota  7334  onminex  7751  tfis  7801  findes  7846  abrexex2g  7912  dfoprab4f  8004  axrepndlem1  10510  axrepndlem2  10511  uzind4s  12853  mo5f  32577  ac6sf2  32714  esumcvg  34250  bj-gabima  37267  wl-lem-moexsb  37911  wl-mo3t  37919  poimirlem26  37985  sbcalf  38453  sbcexf  38454  sbcrexgOLD  43235  scottabes  44691  2sb5nd  45009  2sb5ndALT  45380  2reu8i  47577  dfich2  47934