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

Theorem nfsb 2269
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 axc16nf 2027 . 2  |-  ( A. z  z  =  y  ->  F/ z [ y  /  x ] ph )
2 nfsb.1 . . 3  |-  F/ z
ph
32nfsb4 2219 . 2  |-  ( -. 
A. z  z  =  y  ->  F/ z [ y  /  x ] ph )
41, 3pm2.61i 168 1  |-  F/ z [ y  /  x ] ph
Colors of variables: wff setvar class
Syntax hints:   A.wal 1442   F/wnf 1667   [wsb 1797
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091
This theorem depends on definitions:  df-bi 189  df-an 373  df-ex 1664  df-nf 1668  df-sb 1798
This theorem is referenced by:  hbsb  2270  sb10f  2285  2sb8e  2296  sb8eu  2332  2mo  2380  cbvralf  3013  cbvreu  3017  cbvralsv  3030  cbvrexsv  3031  cbvrab  3043  cbvreucsf  3397  cbvrabcsf  3398  cbvopab1  4473  cbvmptf  4493  cbvmpt  4494  ralxpf  4981  cbviota  5551  sb8iota  5553  cbvriota  6262  dfoprab4f  6851  mo5f  28120  ax11-pm2  31438  2sb5nd  36927
  Copyright terms: Public domain W3C validator