Theorem nfs1v 2160

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

Syntax hints:   → wi 4  ∀wal 1535  Ⅎwnf 1784  [wsb 2069

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-10 2145

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-ex 1781  df-nf 1785  df-sb 2070

This theorem is referenced by:  hbs1  2274  sb5  2276  sbbibOLD  2289  sb8v  2373  sb8ev  2374  sbbib  2380  sb2ae  2536  mo3  2648  eu1  2694  2mo  2733  2eu6  2742  nfsab1  2808  cbvralfw  3437  cbvralf  3439  cbvralsvw  3467  cbvrexsvw  3468  cbvralsv  3469  cbvrexsv  3470  cbvrabw  3489  cbvrab  3490  sbhypf  3552  mob2  3706  reu2  3716  reu2eqd  3727  sbcralt  3855  sbcreu  3859  cbvrabcsfw  3924  cbvreucsf  3927  cbvrabcsf  3928  sbcel12  4360  sbceqg  4361  2nreu  4393  csbif  4522  rexreusng  4617  cbvopab1  5139  cbvopab1g  5140  cbvopab1s  5142  cbvmptf  5165  cbvmptfg  5166  opelopabsb  5417  csbopab  5442  csbopabgALT  5443  opeliunxp  5619  ralxpf  5717  cbviotaw  6321  cbviota  6323  csbiota  6348  isarep1  6442  f1ossf1o  6890  cbvriotaw  7123  cbvriota  7127  csbriota  7129  onminex  7522  tfis  7569  findes  7612  abrexex2g  7665  dfoprab4f  7754  axrepndlem1  10014  axrepndlem2  10015  uzind4s  12309  mo5f  30253  ac6sf2  30370  esumcvg  31345  wl-lem-moexsb  34819  wl-mo3t  34827  poimirlem26  34933  sbcalf  35407  sbcexf  35408  sbcrexgOLD  39431  scottabes  40627  2sb5nd  40943  2sb5ndALT  41315  2reu8i  43361  dfich2  43662  dfich2ai  43663  dfich2OLD  43665  ichnfimlem2  43671  opeliun2xp  44430