Theorem nfs1v 2465

Description: The setvar 𝑥 is not free in [𝑦 / 𝑥]𝜑 when 𝑥 and 𝑦 are distinct. (Contributed by Mario Carneiro, 11-Aug-2016.)

Assertion

Ref	Expression
nfs1v	⊢ Ⅎ𝑥[𝑦 / 𝑥]𝜑

Distinct variable group:   𝑥,𝑦

Allowed substitution hints:   𝜑(𝑥,𝑦)

Proof of Theorem nfs1v

Step	Hyp	Ref	Expression
1		hbs1 2464	. 2 ⊢ ([𝑦 / 𝑥]𝜑 → ∀𝑥[𝑦 / 𝑥]𝜑)
2	1	nf5i 2064	1 ⊢ Ⅎ𝑥[𝑦 / 𝑥]𝜑

Syntax hints:  Ⅎwnf 1748  [wsb 1937

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-10 2059  ax-12 2087  ax-13 2282

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-ex 1745  df-nf 1750  df-sb 1938

This theorem is referenced by:  mo3  2536  eu1  2539  2mo  2580  2eu6  2587  cbvralf  3195  cbvralsv  3212  cbvrexsv  3213  cbvrab  3229  sbhypf  3284  mob2  3419  reu2  3427  reu2eqd  3436  sbcralt  3543  sbcreu  3548  cbvreucsf  3600  cbvrabcsf  3601  sbcel12  4016  sbceqg  4017  csbif  4171  cbvopab1  4756  cbvopab1s  4758  cbvmptf  4781  cbvmpt  4782  opelopabsb  5014  csbopab  5037  csbopabgALT  5038  opeliunxp  5204  ralxpf  5301  cbviota  5894  csbiota  5919  isarep1  6015  cbvriota  6661  csbriota  6663  onminex  7049  tfis  7096  findes  7138  abrexex2g  7186  abrexex2OLD  7192  dfoprab4f  7270  axrepndlem1  9452  axrepndlem2  9453  uzind4s  11786  mo5f  29452  ac6sf2  29557  esumcvg  30276  bj-mo3OLD  32957  wl-lem-moexsb  33480  wl-mo3t  33488  poimirlem26  33565  sbcalf  34047  sbcexf  34048  sbcrexgOLD  37666  sbcel12gOLD  39071  2sb5nd  39093  2sb5ndALT  39482  opeliun2xp  42436