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

Theorem nfsb 2439
 Description: If 𝑧 is not free in 𝜑, it is not free in [𝑦 / 𝑥]𝜑 when 𝑦 and 𝑧 are distinct. (Contributed by Mario Carneiro, 11-Aug-2016.)
Hypothesis
Ref Expression
nfsb.1 𝑧𝜑
Assertion
Ref Expression
nfsb 𝑧[𝑦 / 𝑥]𝜑
Distinct variable group:   𝑦,𝑧
Allowed substitution hints:   𝜑(𝑥,𝑦,𝑧)

Proof of Theorem nfsb
StepHypRef Expression
1 axc16nf 2133 . 2 (∀𝑧 𝑧 = 𝑦 → Ⅎ𝑧[𝑦 / 𝑥]𝜑)
2 nfsb.1 . . 3 𝑧𝜑
32nfsb4 2389 . 2 (¬ ∀𝑧 𝑧 = 𝑦 → Ⅎ𝑧[𝑦 / 𝑥]𝜑)
41, 3pm2.61i 176 1 𝑧[𝑦 / 𝑥]𝜑
 Colors of variables: wff setvar class Syntax hints:  ∀wal 1478  Ⅎwnf 1705  [wsb 1877 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245 This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878 This theorem is referenced by:  hbsb  2440  sb10f  2455  2sb8e  2466  sb8eu  2502  2mo  2550  cbvralf  3153  cbvreu  3157  cbvralsv  3170  cbvrexsv  3171  cbvrab  3184  cbvreucsf  3548  cbvrabcsf  3549  cbvopab1  4685  cbvmptf  4708  cbvmpt  4709  ralxpf  5228  cbviota  5815  sb8iota  5817  cbvriota  6575  dfoprab4f  7171  mo5f  29173  ax11-pm2  32466  2sb5nd  38258
 Copyright terms: Public domain W3C validator