MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  nfsb Structured version   Unicode version

Theorem nfsb 2208
Description: If  z is not free in  ph, it is not free in  [ y  /  x ] ph when  y and  z are distinct. (Contributed by Mario Carneiro, 11-Aug-2016.)
Hypothesis
Ref Expression
nfsb.1  |-  F/ z
ph
Assertion
Ref Expression
nfsb  |-  F/ z [ y  /  x ] ph
Distinct variable group:    y, z
Allowed substitution hints:    ph( x, y, z)

Proof of Theorem nfsb
StepHypRef Expression
1 ax16nf 1972 . 2  |-  ( A. z  z  =  y  ->  F/ z [ y  /  x ] ph )
2 nfsb.1 . . 3  |-  F/ z
ph
32nfsb4 2155 . 2  |-  ( -. 
A. z  z  =  y  ->  F/ z [ y  /  x ] ph )
41, 3pm2.61i 164 1  |-  F/ z [ y  /  x ] ph
Colors of variables: wff setvar class
Syntax hints:   A.wal 1403   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-11 1866  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:  hbsb  2209  sb10f  2224  2sb8e  2235  sb8eu  2273  sb8euOLD  2274  2mo  2324  2moOLD  2325  2eu6OLD  2335  cbvabOLD  2544  cbvralf  3028  cbvreu  3032  cbvralsv  3045  cbvrexsv  3046  cbvrab  3057  cbvreucsf  3407  cbvrabcsf  3408  cbvopab1  4465  cbvmptf  4485  cbvmpt  4486  ralxpf  4970  cbviota  5538  sb8iota  5540  cbvriota  6250  dfoprab4f  6842  mo5f  27798  ax11-pm2  30973  2sb5nd  36357
  Copyright terms: Public domain W3C validator