Theorem nfs1v 2193

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

This proof depends on syntax axioms:   → wi 4  ∀wal 1568  Ⅎwnf 1816  [wsb 2099

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-10 2178

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-ex 1813  df-nf 1817  df-sb 2100

This theorem is used by:  hbs1  2308  sb8ef  2385  sbbib  2391  sb2ae  2526  mo3  2590  eu1  2636  2mo  2674  2eu6  2682  nfsab1  2747  cbvrexsvw  3315  cbvralf  3346  cbvralsv  3352  cbvrexsv  3353  cbvrab  3450  mob2  3673  reu2  3683  reu2eqd  3694  sbcralt  3819  sbcreu  3823  cbvrabcsfw  3888  cbvreucsf  3891  cbvrabcsf  3892  sbcel12  4369  sbceqg  4370  2nreu  4402  csbif  4540  rexreusng  4640  cbvopab1  5179  cbvopab1g  5180  cbvopab1s  5182  cbvmptf  5205  cbvmptfg  5206  csbopab  5530  csbopabw  5531  opeliunxp  5718  opeliun2xp  5719  ralxpf  5824  cbviotaw  6501  cbviota  6503  csbiota  6531  isarep1  6628  f1ossf1o  7129  cbvriotaw  7386  cbvriota  7390  csbriota  7392  onminex  7816  tfis  7866  findes  7912  abrexex2g  7976  dfoprab4f  8067  scottabes  9941  axrepndlem1  10677  axrepndlem2  10678  uzind4s  13035  mo5f  33085  ac6sf2  33216  esumcvg  34718  bj-gabima  37853  wl-lem-moexsb  38500  wl-mo3t  38508  poimirlem26  38564  sbcalf  39046  sbcexf  39047  2sb5nd  45542  2sb5ndALT  45913  2reu8i  48182  dfich2  48539