Theorem nfs1v 2195

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

This proof depends on syntax axioms:   → wi 4  ∀wal 1567  Ⅎwnf 1815  [wsb 2100

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-10 2179

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-ex 1812  df-nf 1816  df-sb 2101

This theorem is used by:  hbs1  2310  sb8ef  2387  sbbib  2393  sb2ae  2528  mo3  2592  eu1  2638  2mo  2676  2eu6  2684  nfsab1  2749  cbvrexsvw  3318  cbvralf  3349  cbvralsv  3355  cbvrexsv  3356  cbvrab  3453  mob2  3676  reu2  3686  reu2eqd  3697  sbcralt  3823  sbcreu  3827  cbvrabcsfw  3892  cbvreucsf  3895  cbvrabcsf  3896  sbcel12  4372  sbceqg  4373  2nreu  4405  csbif  4543  rexreusng  4640  cbvopab1  5182  cbvopab1g  5183  cbvopab1s  5185  cbvmptf  5208  cbvmptfg  5209  csbopab  5534  csbopabw  5535  opeliunxp  5722  opeliun2xp  5723  ralxpf  5829  cbviotaw  6508  cbviota  6510  csbiota  6540  isarep1  6639  f1ossf1o  7140  cbvriotaw  7396  cbvriota  7400  csbriota  7402  onminex  7826  tfis  7876  findes  7922  abrexex2g  7986  dfoprab4f  8078  scottabes  9954  axrepndlem1  10690  axrepndlem2  10691  uzind4s  13048  mo5f  33142  ac6sf2  33273  esumcvg  34774  bj-gabima  37986  wl-lem-moexsb  38646  wl-mo3t  38654  poimirlem26  38710  sbcalf  39192  sbcexf  39193  2sb5nd  45688  2sb5ndALT  46059  2reu8i  48329  dfich2  48685