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

Theorem nfsb 2155
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 1882 . 2  |-  ( A. z  z  =  y  ->  F/ z [ y  /  x ] ph )
2 nfsb.1 . . 3  |-  F/ z
ph
32nfsb4 2091 . 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 1368   F/wnf 1590   [wsb 1702
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1588  df-nf 1591  df-sb 1703
This theorem is referenced by:  hbsb  2156  2sb5rfOLD  2170  2sb6rfOLD  2171  sb10f  2175  2sb8e  2189  sb8eu  2301  sb8euOLD  2302  sb8euOLDOLD  2303  2mo  2369  2moOLD  2370  2moOLDOLD  2371  2eu6OLD  2381  cbvabOLD  2596  cbvralf  3047  cbvreu  3051  cbvralsv  3064  cbvrexsv  3065  cbvrab  3076  cbvreucsf  3432  cbvrabcsf  3433  cbvopab1  4473  cbvmpt  4493  ralxpf  5097  cbviota  5497  sb8iota  5499  cbvriota  6174  dfoprab4f  6745  mo5f  26047  cbvmptf  26149  2sb5nd  31624  ax11-pm2  32701
  Copyright terms: Public domain W3C validator