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  2359  sbbib  2365  sb2ae  2500  mo3  2564  eu1  2610  2mo  2648  2eu6  2657  nfsab1  2722  cbvrexsvw  3289  cbvralsvwOLD  3290  cbvralf  3322  cbvralsv  3328  cbvrexsv  3329  cbvrabwOLD  3425  cbvrab  3428  mob2  3661  reu2  3671  reu2eqd  3682  sbcralt  3810  sbcreu  3814  cbvrabcsfw  3878  cbvreucsf  3881  cbvrabcsf  3882  sbcel12  4351  sbceqg  4352  2nreu  4384  csbif  4524  rexreusng  4623  cbvopab1  5159  cbvopab1g  5160  cbvopab1s  5162  cbvmptf  5185  cbvmptfg  5186  csbopab  5510  csbopabgALT  5511  opeliunxp  5698  opeliun2xp  5699  ralxpf  5801  cbviotaw  6461  cbviota  6463  csbiota  6491  isarep1  6587  f1ossf1o  7081  cbvriotaw  7333  cbvriota  7337  csbriota  7339  onminex  7756  tfis  7806  findes  7851  abrexex2g  7917  dfoprab4f  8009  axrepndlem1  10515  axrepndlem2  10516  uzind4s  12858  mo5f  32558  ac6sf2  32695  esumcvg  34230  bj-gabima  37247  wl-lem-moexsb  37893  wl-mo3t  37901  poimirlem26  37967  sbcalf  38435  sbcexf  38436  scottabes  44669  2sb5nd  44987  2sb5ndALT  45358  2reu8i  47561  dfich2  47918