Theorem nfs1v 2167

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

Syntax hints:   → wi 4  ∀wal 1545  Ⅎwnf 1790  [wsb 2073

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-10 2152

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-ex 1787  df-nf 1791  df-sb 2074

This theorem is referenced by:  hbs1  2285  sb8ef  2363  sbbib  2369  sb2ae  2504  mo3  2568  eu1  2614  2mo  2652  2eu6  2660  nfsab1  2725  cbvrexsvw  3291  cbvralsvwOLD  3292  cbvralf  3324  cbvralsv  3330  cbvrexsv  3331  cbvrabwOLD  3427  cbvrab  3430  mob2  3656  reu2  3666  reu2eqd  3677  sbcralt  3804  sbcreu  3808  cbvrabcsfw  3872  cbvreucsf  3875  cbvrabcsf  3876  sbcel12  4340  sbceqg  4341  2nreu  4373  csbif  4513  rexreusng  4612  cbvopab1  5147  cbvopab1g  5148  cbvopab1s  5150  cbvmptf  5173  cbvmptfg  5174  csbopab  5498  csbopabgALT  5499  opeliunxp  5686  opeliun2xp  5687  ralxpf  5789  cbviotaw  6449  cbviota  6451  csbiota  6479  isarep1  6575  f1ossf1o  7071  cbvriotaw  7323  cbvriota  7327  csbriota  7329  onminex  7746  tfis  7796  findes  7841  abrexex2g  7907  dfoprab4f  7999  axrepndlem1  10507  axrepndlem2  10508  uzind4s  12850  mo5f  32577  ac6sf2  32715  esumcvg  34279  bj-gabima  37302  wl-lem-moexsb  37948  wl-mo3t  37956  poimirlem26  38022  sbcalf  38490  sbcexf  38491  scottabes  44695  2sb5nd  45013  2sb5ndALT  45384  2reu8i  47584  dfich2  47941