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

Theorem nfsb 2523
Description: If 𝑧 is not free in 𝜑, then it is not free in [𝑦 / 𝑥]𝜑 when 𝑦 and 𝑧 are distinct. See nfsbv 2324 for a version with an additional disjoint variable condition on 𝑥, 𝑧 but not requiring ax-13 2372. (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof shortened by Wolf Lammen, 25-Feb-2024.) Usage of this theorem is discouraged because it depends on ax-13 2372. Use nfsbv 2324 instead. (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 1807 . . 3 𝑥
2 nfsb.1 . . . 4 𝑧𝜑
32a1i 11 . . 3 (⊤ → Ⅎ𝑧𝜑)
41, 3nfsbd 2522 . 2 (⊤ → Ⅎ𝑧[𝑦 / 𝑥]𝜑)
54mptru 1549 1 𝑧[𝑦 / 𝑥]𝜑
Colors of variables: wff setvar class
Syntax hints:  wtru 1543  wnf 1786  [wsb 2068
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-10 2138  ax-11 2155  ax-12 2172  ax-13 2372
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-ex 1783  df-nf 1787  df-sb 2069
This theorem is referenced by:  hbsb  2524  sb10f  2527  2sb8e  2530  sb8eu  2595  cbvralf  3357  cbvralsv  3363  cbvrexsv  3364  cbvreu  3425  cbvrab  3474  cbvreucsf  3941  cbvrabcsf  3942  cbvopab1g  5225  cbvmptfg  5259  cbviota  6506  sb8iota  6508  cbvriota  7379  2sb5nd  43321
  Copyright terms: Public domain W3C validator