Theorem nfs1v 2277

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

Syntax hints:   → wi 4  ∀wal 1632  Ⅎwnf 1859  [wsb 2052

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1873  ax-4 1888  ax-5 1994  ax-6 2060  ax-7 2096  ax-10 2177  ax-12 2206

This theorem depends on definitions:  df-bi 198  df-an 384  df-or 864  df-ex 1856  df-nf 1861  df-sb 2053

This theorem is referenced by:  hbs1  2278  mo3  2659  eu1  2662  2mo  2703  2eu6  2710  cbvralf  3318  cbvralsv  3335  cbvrexsv  3336  cbvrab  3352  sbhypf  3410  mob2  3544  reu2  3552  reu2eqd  3561  sbcralt  3666  sbcreu  3670  cbvreucsf  3722  cbvrabcsf  3723  sbcel12  4137  sbceqg  4138  csbif  4287  cbvopab1  4870  cbvopab1s  4872  cbvmptf  4895  cbvmpt  4896  opelopabsb  5132  csbopab  5155  csbopabgALT  5156  opeliunxp  5322  ralxpf  5419  cbviota  6010  csbiota  6035  isarep1  6128  f1ossf1o  6556  cbvriota  6783  csbriota  6785  onminex  7175  tfis  7222  findes  7264  abrexex2g  7312  abrexex2OLD  7318  dfoprab4f  7396  axrepndlem1  9637  axrepndlem2  9638  uzind4s  11972  mo5f  29681  ac6sf2  29786  esumcvg  30505  bj-mo3OLD  33183  wl-lem-moexsb  33701  wl-mo3t  33709  poimirlem26  33785  sbcalf  34265  sbcexf  34266  sbcrexgOLD  37890  sbcel12gOLD  39292  2sb5nd  39314  2sb5ndALT  39702  euabsneu  41696  opeliun2xp  42663