Theorem nfs1v 2157

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

Syntax hints:   → wi 4  ∀wal 1538  Ⅎwnf 1783  [wsb 2065

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-10 2142

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1780  df-nf 1784  df-sb 2066

This theorem is referenced by:  hbs1  2274  sb8ef  2353  sbbib  2359  sb2ae  2494  mo3  2557  eu1  2603  2mo  2641  2eu6  2650  nfsab1  2715  cbvrexsvw  3281  cbvralsvwOLD  3282  cbvralsvwOLDOLD  3283  cbvrexsvwOLD  3284  cbvralf  3323  cbvralsv  3329  cbvrexsv  3330  cbvrabwOLD  3431  cbvrab  3435  sbhypfOLD  3500  mob2  3675  reu2  3685  reu2eqd  3696  sbcralt  3824  sbcreu  3828  cbvrabcsfw  3892  cbvreucsf  3895  cbvrabcsf  3896  sbcel12  4362  sbceqg  4363  2nreu  4395  csbif  4534  rexreusng  4631  cbvopab1  5166  cbvopab1g  5167  cbvopab1s  5169  cbvmptf  5192  cbvmptfg  5193  csbopab  5498  csbopabgALT  5499  opeliunxp  5686  opeliun2xp  5687  ralxpf  5789  cbviotaw  6445  cbviota  6447  csbiota  6475  isarep1  6571  f1ossf1o  7062  cbvriotaw  7315  cbvriota  7319  csbriota  7321  onminex  7738  tfis  7788  findes  7833  abrexex2g  7899  dfoprab4f  7991  axrepndlem1  10486  axrepndlem2  10487  uzind4s  12809  mo5f  32433  ac6sf2  32567  esumcvg  34059  bj-gabima  36924  wl-lem-moexsb  37552  wl-mo3t  37560  poimirlem26  37636  sbcalf  38104  sbcexf  38105  sbcrexgOLD  42768  scottabes  44225  2sb5nd  44544  2sb5ndALT  44915  2reu8i  47107  dfich2  47452