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

Theorem nfsb 2528
Description: If 𝑧 is not free in 𝜑, then it is not free in [𝑦 / 𝑥]𝜑 when 𝑦 and 𝑧 are distinct. See nfsbv 2330 for a version with an additional disjoint variable condition on 𝑥, 𝑧 but not requiring ax-13 2377. (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 2377. Use nfsbv 2330 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 1804 . . 3 𝑥
2 nfsb.1 . . . 4 𝑧𝜑
32a1i 11 . . 3 (⊤ → Ⅎ𝑧𝜑)
41, 3nfsbd 2527 . 2 (⊤ → Ⅎ𝑧[𝑦 / 𝑥]𝜑)
54mptru 1547 1 𝑧[𝑦 / 𝑥]𝜑
Colors of variables: wff setvar class
Syntax hints:  wtru 1541  wnf 1783  [wsb 2064
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-10 2141  ax-11 2157  ax-12 2177  ax-13 2377
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1543  df-ex 1780  df-nf 1784  df-sb 2065
This theorem is referenced by:  hbsb  2529  sb10f  2532  2sb8e  2535  sb8eu  2600  cbvralf  3360  cbvralsv  3366  cbvrexsv  3367  cbvreu  3428  cbvrab  3479  cbvreucsf  3943  cbvrabcsf  3944  cbvopab1g  5218  cbvmptfg  5252  cbviota  6523  sb8iota  6525  cbvriota  7401  2sb5nd  44580
  Copyright terms: Public domain W3C validator