Theorem nfs1v 2313

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

Syntax hints:   → wi 4  ∀wal 1656  Ⅎwnf 1884  [wsb 2069

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-10 2194  ax-12 2222

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 881  df-ex 1881  df-nf 1885  df-sb 2070

This theorem is referenced by:  hbs1  2314  sb8v  2378  sb8ev  2379  mo3  2633  mo3OLD  2634  eu1  2695  eu1OLD  2696  2mo  2731  2eu6  2738  cbvralf  3377  cbvralsv  3394  cbvrexsv  3395  cbvrab  3411  sbhypf  3470  mob2  3611  reu2  3619  reu2eqd  3630  sbcralt  3735  sbcreu  3739  cbvreucsf  3791  cbvrabcsf  3792  sbcel12  4207  sbceqg  4208  csbif  4361  cbvopab1  4946  cbvopab1s  4948  cbvmptf  4971  cbvmpt  4972  opelopabsb  5211  csbopab  5234  csbopabgALT  5235  opeliunxp  5403  ralxpf  5501  cbviota  6091  csbiota  6116  isarep1  6210  f1ossf1o  6645  cbvriota  6876  csbriota  6878  onminex  7268  tfis  7315  findes  7357  abrexex2g  7405  dfoprab4f  7488  axrepndlem1  9729  axrepndlem2  9730  uzind4s  12030  mo5f  29879  ac6sf2  29978  esumcvg  30693  bj-mo3OLD  33356  wl-lem-moexsb  33894  wl-mo3t  33902  poimirlem26  33979  sbcalf  34458  sbcexf  34459  sbcrexgOLD  38193  2sb5nd  39604  2sb5ndALT  39986  opeliun2xp  42958