Theorem nfs1v 2153

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

Syntax hints:   → wi 4  ∀wal 1537  Ⅎwnf 1786  [wsb 2067

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-10 2137

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-ex 1783  df-nf 1787  df-sb 2068

This theorem is referenced by:  hbs1  2266  sb5OLD  2269  sb8fOLD  2352  sb8ef  2353  sbbib  2359  sb2ae  2500  mo3  2564  eu1  2612  2mo  2650  2eu6  2658  nfsab1  2723  cbvralfwOLD  3369  cbvralf  3371  cbvralsvw  3402  cbvrexsvw  3403  cbvralsv  3404  cbvrexsv  3405  cbvrabw  3424  cbvrab  3425  sbhypf  3491  mob2  3650  reu2  3660  reu2eqd  3671  sbcralt  3805  sbcreu  3809  cbvrabcsfw  3876  cbvreucsf  3879  cbvrabcsf  3880  sbcel12  4342  sbceqg  4343  2nreu  4375  csbif  4516  rexreusng  4615  cbvopab1  5149  cbvopab1g  5150  cbvopab1s  5152  cbvmptf  5183  cbvmptfg  5184  csbopab  5468  csbopabgALT  5469  opeliunxp  5654  ralxpf  5755  cbviotaw  6398  cbviota  6401  csbiota  6426  isarep1  6522  f1ossf1o  7000  cbvriotaw  7241  cbvriota  7246  csbriota  7248  onminex  7652  tfis  7701  findes  7749  abrexex2g  7807  dfoprab4f  7896  axrepndlem1  10348  axrepndlem2  10349  uzind4s  12648  mo5f  30837  ac6sf2  30960  esumcvg  32054  bj-gabima  35128  wl-lem-moexsb  35723  wl-mo3t  35731  poimirlem26  35803  sbcalf  36272  sbcexf  36273  sbcrexgOLD  40607  scottabes  41860  2sb5nd  42180  2sb5ndALT  42552  2reu8i  44605  dfich2  44910  opeliun2xp  45668