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

Theorem nfsb 2545
 Description: If 𝑧 is not free in 𝜑, it is not free in [𝑦 / 𝑥]𝜑 when 𝑦 and 𝑧 are distinct. Usage of this theorem is discouraged because it depends on ax-13 2382. For a version requiring more disjoint variables, but fewer axioms, see nfsbv 2341. (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof shortened by Wolf Lammen, 25-Feb-2024.) (New usage is discouraged.)
Hypothesis
Ref Expression
nfsb.1 𝑧𝜑
Assertion
Ref Expression
nfsb 𝑧[𝑦 / 𝑥]𝜑
Distinct variable group:   𝑦,𝑧
Allowed substitution hints:   𝜑(𝑥,𝑦,𝑧)

Proof of Theorem nfsb
StepHypRef Expression
1 nftru 1806 . . 3 𝑥
2 nfsb.1 . . . 4 𝑧𝜑
32a1i 11 . . 3 (⊤ → Ⅎ𝑧𝜑)
41, 3nfsbd 2544 . 2 (⊤ → Ⅎ𝑧[𝑦 / 𝑥]𝜑)
54mptru 1545 1 𝑧[𝑦 / 𝑥]𝜑
 Colors of variables: wff setvar class Syntax hints:  ⊤wtru 1539  Ⅎwnf 1785  [wsb 2069 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-10 2143  ax-11 2159  ax-12 2176  ax-13 2382 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070 This theorem is referenced by:  hbsb  2547  sb10f  2550  2sb8e  2555  sb8eu  2664  cbvralf  3388  cbvreu  3397  cbvralsv  3419  cbvrexsv  3420  cbvrab  3441  cbvreucsf  3875  cbvrabcsf  3876  cbvopab1g  5107  cbvmptfg  5133  cbviota  6296  sb8iota  6298  cbvriota  7110  2sb5nd  41259
 Copyright terms: Public domain W3C validator