Theorem nfs1v 2205

Description: x is not free in [ y / x ] ph when x and y are distinct. (Contributed by Mario Carneiro, 11-Aug-2016.)

Assertion

Ref	Expression
nfs1v	|- F/ x [ y / x ] ph

Distinct variable group:   x, y

Allowed substitution hints:   ph( x, y)

Proof of Theorem nfs1v

Step	Hyp	Ref	Expression
1		hbs1 2204	. 2 |- ( [ y / x ] ph -> A. x [ y / x ] ph )
2	1	nfi 1644	1 |- F/ x [ y / x ] ph

Syntax hints:   F/wnf 1637   [wsb 1763

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-10 1861  ax-12 1878  ax-13 2026

This theorem depends on definitions:  df-bi 185  df-an 369  df-ex 1634  df-nf 1638  df-sb 1764

This theorem is referenced by:  mo3  2278  mo3OLD  2279  eu1  2282  2mo  2324  2moOLD  2325  2eu6  2334  2eu6OLD  2335  clelabOLD  2547  cbvralf  3028  cbvralsv  3045  cbvrexsv  3046  cbvrab  3057  sbhypf  3106  mob2  3229  reu2  3237  reu2eqd  3246  sbcralt  3350  sbcreu  3354  cbvreucsf  3407  cbvrabcsf  3408  sbcel12  3777  sbceqg  3778  csbif  3935  rabasiun  4275  cbvopab1  4465  cbvopab1s  4467  cbvmptf  4485  cbvmpt  4486  opelopabsb  4700  csbopab  4722  csbopabgALT  4723  opeliunxp  4875  ralxpf  4970  cbviota  5538  csbiota  5562  isarep1  5648  cbvriota  6250  csbriota  6252  onminex  6625  tfis  6672  findes  6714  abrexex2g  6761  abrexex2  6765  dfoprab4f  6842  axrepndlem1  8999  axrepndlem2  9000  uzind4s  11187  mo5f  27798  ac6sf2  27909  esumcvg  28533  wl-lem-moexsb  31384  wl-mo3t  31388  sbcalf  31799  sbcexf  31800  sbcrexgOLD  35080  sbcel12gOLD  36335  2sb5nd  36357  2sb5ndALT  36763  opeliun2xp  38433