Theorem nfs1v 2194

Description: The setvar 𝑥 is not free in [𝑦 / 𝑥]𝜑 when 𝑥 and 𝑦 are distinct. (Contributed by Mario Carneiro, 11-Aug-2016.) Shorten nfs1v 2194 and hbs1 2311 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 2189	. 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 2179

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  2311  sb8ef  2389  sbbib  2395  sb2ae  2530  mo3  2594  eu1  2640  2mo  2678  2eu6  2686  nfsab1  2751  cbvrexsvw  3319  cbvralsvwOLD  3320  cbvralf  3351  cbvralsv  3357  cbvrexsv  3358  cbvrab  3456  mob2  3680  reu2  3690  reu2eqd  3701  sbcralt  3826  sbcreu  3830  cbvrabcsfw  3895  cbvreucsf  3898  cbvrabcsf  3899  sbcel12  4376  sbceqg  4377  2nreu  4409  csbif  4547  rexreusng  4647  cbvopab1  5187  cbvopab1g  5188  cbvopab1s  5190  cbvmptf  5213  cbvmptfg  5214  csbopab  5542  csbopabw  5543  opeliunxp  5730  opeliun2xp  5731  ralxpf  5834  cbviotaw  6503  cbviota  6505  csbiota  6533  isarep1  6628  f1ossf1o  7128  cbvriotaw  7385  cbvriota  7389  csbriota  7391  onminex  7807  tfis  7857  findes  7903  abrexex2g  7967  dfoprab4f  8059  scottabes  9877  axrepndlem1  10596  axrepndlem2  10597  uzind4s  12952  mo5f  32910  ac6sf2  33042  esumcvg  34544  bj-gabima  37637  wl-lem-moexsb  38284  wl-mo3t  38292  poimirlem26  38358  sbcalf  38825  sbcexf  38826  2sb5nd  45346  2sb5ndALT  45717  2reu8i  47927  dfich2  48284