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

Theorem nfsb 2521
Description: If 𝑧 is not free in 𝜑, then it is not free in [𝑦 / 𝑥]𝜑 when 𝑦 and 𝑧 are distinct. See nfsbv 2322 for a version with an additional disjoint variable condition on 𝑥, 𝑧 but not requiring ax-13 2370. (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 2370. Use nfsbv 2322 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 1805 . . 3 𝑥
2 nfsb.1 . . . 4 𝑧𝜑
32a1i 11 . . 3 (⊤ → Ⅎ𝑧𝜑)
41, 3nfsbd 2520 . 2 (⊤ → Ⅎ𝑧[𝑦 / 𝑥]𝜑)
54mptru 1547 1 𝑧[𝑦 / 𝑥]𝜑
Colors of variables: wff setvar class
Syntax hints:  wtru 1541  wnf 1784  [wsb 2066
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-10 2136  ax-11 2153  ax-12 2170  ax-13 2370
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-tru 1543  df-ex 1781  df-nf 1785  df-sb 2067
This theorem is referenced by:  hbsb  2522  sb10f  2525  2sb8e  2528  sb8eu  2593  cbvralf  3355  cbvralsv  3361  cbvrexsv  3362  cbvreu  3423  cbvrab  3472  cbvreucsf  3940  cbvrabcsf  3941  cbvopab1g  5224  cbvmptfg  5258  cbviota  6505  sb8iota  6507  cbvriota  7382  2sb5nd  43624
  Copyright terms: Public domain W3C validator