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

Theorem nfsb 2236
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 2001 . 2  |-  ( A. z  z  =  y  ->  F/ z [ y  /  x ] ph )
2 nfsb.1 . . 3  |-  F/ z
ph
32nfsb4 2185 . 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 1436   F/wnf 1664   [wsb 1787
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-5 1749  ax-6 1795  ax-7 1840  ax-10 1888  ax-11 1893  ax-12 1906  ax-13 2054
This theorem depends on definitions:  df-bi 189  df-an 373  df-ex 1661  df-nf 1665  df-sb 1788
This theorem is referenced by:  hbsb  2237  sb10f  2252  2sb8e  2263  sb8eu  2300  2mo  2348  2moOLD  2349  cbvabOLD  2565  cbvralf  3050  cbvreu  3054  cbvralsv  3067  cbvrexsv  3068  cbvrab  3080  cbvreucsf  3430  cbvrabcsf  3431  cbvopab1  4492  cbvmptf  4512  cbvmpt  4513  ralxpf  4998  cbviota  5568  sb8iota  5570  cbvriota  6275  dfoprab4f  6863  mo5f  28112  ax11-pm2  31402  2sb5nd  36829
  Copyright terms: Public domain W3C validator