Theorem nfs1v 2155

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

Syntax hints:   → wi 4  ∀wal 1537  Ⅎwnf 1782  [wsb 2063

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-10 2140

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1779  df-nf 1783  df-sb 2064

This theorem is referenced by:  hbs1  2273  sb8fOLD  2355  sb8ef  2356  sbbib  2362  sb2ae  2499  mo3  2562  eu1  2608  2mo  2646  2eu6  2655  nfsab1  2720  cbvrexsvw  3301  cbvralsvwOLD  3302  cbvralsvwOLDOLD  3303  cbvrexsvwOLD  3304  cbvralf  3343  cbvralsv  3349  cbvrexsv  3350  cbvrabwOLD  3457  cbvrab  3462  sbhypfOLD  3528  mob2  3703  reu2  3713  reu2eqd  3724  sbcralt  3852  sbcreu  3856  cbvrabcsfw  3920  cbvreucsf  3923  cbvrabcsf  3924  sbcel12  4391  sbceqg  4392  2nreu  4424  csbif  4563  rexreusng  4659  cbvopab1  5197  cbvopab1g  5198  cbvopab1s  5200  cbvmptf  5231  cbvmptfg  5232  csbopab  5540  csbopabgALT  5541  opeliunxp  5732  opeliun2xp  5733  ralxpf  5837  cbviotaw  6500  cbviota  6502  csbiota  6533  isarep1  6635  isarep1OLD  6636  f1ossf1o  7127  cbvriotaw  7378  cbvriota  7382  csbriota  7384  onminex  7803  tfis  7857  findes  7903  abrexex2g  7970  dfoprab4f  8062  axrepndlem1  10613  axrepndlem2  10614  uzind4s  12931  mo5f  32435  ac6sf2  32561  esumcvg  34021  bj-gabima  36875  wl-lem-moexsb  37503  wl-mo3t  37511  poimirlem26  37587  sbcalf  38055  sbcexf  38056  sbcrexgOLD  42734  scottabes  44194  2sb5nd  44513  2sb5ndALT  44885  2reu8i  47059  dfich2  47379