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

Theorem nfsb 2605
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 2316 . 2 (∀𝑧 𝑧 = 𝑦 → Ⅎ𝑧[𝑦 / 𝑥]𝜑)
2 nfsb.1 . . 3 𝑧𝜑
32nfsb4 2551 . 2 (¬ ∀𝑧 𝑧 = 𝑦 → Ⅎ𝑧[𝑦 / 𝑥]𝜑)
41, 3pm2.61i 176 1 𝑧[𝑦 / 𝑥]𝜑
Colors of variables: wff setvar class
Syntax hints:  wal 1635  wnf 1863  [wsb 2061
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062
This theorem is referenced by:  hbsb  2606  sb10f  2619  2sb8e  2630  sb8eu  2677  2mo  2726  cbvralf  3365  cbvreu  3369  cbvralsv  3382  cbvrexsv  3383  cbvrab  3399  cbvreucsf  3773  cbvrabcsf  3774  cbvopab1  4928  cbvmptf  4953  cbvmpt  4954  ralxpf  5483  cbviota  6078  sb8iota  6080  cbvriota  6854  dfoprab4f  7467  mo5f  29674  ax11-pm2  33154  2sb5nd  39291
  Copyright terms: Public domain W3C validator