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

Theorem nfsb 2148
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 2012 . 2  |-  ( A. z  z  =  y  ->  F/ z [ y  /  x ] ph )
2 nfsb.1 . . 3  |-  F/ z
ph
32nfsb4 2079 . 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 1360   F/wnf 1592   [wsb 1699
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1590  df-nf 1593  df-sb 1700
This theorem is referenced by:  hbsb  2149  2sb5rfOLD  2163  2sb6rfOLD  2164  sb10f  2168  sb8eu  2289  sb8euOLD  2290  2mo  2355  2moOLD  2356  2eu6  2363  cbvab  2551  cbvralf  2931  cbvreu  2935  cbvralsv  2948  cbvrexsv  2949  cbvrab  2960  cbvreucsf  3309  cbvrabcsf  3310  cbvopab1  4350  cbvmpt  4370  ralxpf  4973  cbviota  5374  sb8iota  5376  cbvriota  6050  dfoprab4f  6621  mo5f  25692  cbvmptf  25795  2sb5nd  30991  ax11-pm2  31985
  Copyright terms: Public domain W3C validator