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

Theorem nfsb 2048
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 1991 . 2  |-  ( A. z  z  =  y  ->  F/ z [ y  /  x ] ph )
2 nfsb.1 . . 3  |-  F/ z
ph
32nfsb4 2021 . 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 1527   F/wnf 1531   [wsb 1629
This theorem is referenced by:  hbsb  2049  2sb5rf  2056  2sb6rf  2057  sb10f  2061  sb8eu  2161  2mo  2221  2eu6  2228  cbvab  2401  cbvralf  2758  cbvreu  2762  cbvralsv  2775  cbvrexsv  2776  cbvrab  2786  cbvreucsf  3145  cbvrabcsf  3146  cbvopab1  4089  cbvmpt  4110  ralxpf  4830  cbviota  5224  sb8iota  5226  dfoprab4f  6178  cbvriota  6315  mo5f  23143  cbvmptf  23220  2sb5nd  28326
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630
  Copyright terms: Public domain W3C validator