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

Theorem nfsb 2061
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 a16nf 2004 . 2  |-  ( A. z  z  =  y  ->  F/ z [ y  /  x ] ph )
2 nfsb.1 . . 3  |-  F/ z
ph
32nfsb4 2034 . 2  |-  ( -. 
A. z  z  =  y  ->  F/ z [ y  /  x ] ph )
41, 3pm2.61i 156 1  |-  F/ z [ y  /  x ] ph
Colors of variables: wff set class
Syntax hints:   A.wal 1530   F/wnf 1534   [wsb 1638
This theorem is referenced by:  hbsb  2062  2sb5rf  2069  2sb6rf  2070  sb10f  2074  sb8eu  2174  2mo  2234  2eu6  2241  cbvab  2414  cbvralf  2771  cbvreu  2775  cbvralsv  2788  cbvrexsv  2789  cbvrab  2799  cbvreucsf  3158  cbvrabcsf  3159  cbvopab1  4105  cbvmpt  4126  ralxpf  4846  cbviota  5240  sb8iota  5242  dfoprab4f  6194  cbvriota  6331  mo5f  23159  cbvmptf  23235  2sb5nd  28625
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639
  Copyright terms: Public domain W3C validator