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

Theorem nfsbv 2319
Description: If 𝑧 is not free in 𝜑, then it is not free in [𝑦 / 𝑥]𝜑 when 𝑧 is disjoint from both 𝑥 and 𝑦. Version of nfsb 2522 with an additional disjoint variable condition on 𝑥, 𝑧 but not requiring ax-13 2367. (Contributed by Mario Carneiro, 11-Aug-2016.) (Revised by Wolf Lammen, 7-Feb-2023.) Remove disjoint variable condition on 𝑥, 𝑦. (Revised by Steven Nguyen, 13-Aug-2023.) (Proof shortened by Wolf Lammen, 25-Oct-2024.)
Hypothesis
Ref Expression
nfsbv.nf 𝑧𝜑
Assertion
Ref Expression
nfsbv 𝑧[𝑦 / 𝑥]𝜑
Distinct variable groups:   𝑥,𝑧   𝑦,𝑧
Allowed substitution hints:   𝜑(𝑥,𝑦,𝑧)

Proof of Theorem nfsbv
StepHypRef Expression
1 nfsbv.nf . . . 4 𝑧𝜑
21nf5ri 2183 . . 3 (𝜑 → ∀𝑧𝜑)
32hbsbw 2164 . 2 ([𝑦 / 𝑥]𝜑 → ∀𝑧[𝑦 / 𝑥]𝜑)
43nf5i 2137 1 𝑧[𝑦 / 𝑥]𝜑
Colors of variables: wff setvar class
Syntax hints:  wnf 1781  [wsb 2062
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-10 2132  ax-11 2149  ax-12 2166
This theorem depends on definitions:  df-bi 206  df-ex 1778  df-nf 1782  df-sb 2063
This theorem is referenced by:  hbsbwOLD  2321  sbco2v  2322  2sb8ef  2349  sb8euv  2594  2mo  2645  nfcriiOLD  2895  cbvralfwOLD  3371  cbvreuwOLD  3379  cbvrabw  3426  cbvrabcsfw  3878  cbvopab1  5152  cbvmptf  5186  ralxpf  5759  cbviotaw  6406  cbvriotaw  7261  dfoprab4f  7916  mo5f  30865  ax11-pm2  35047  dfich2  44950  ichbi12i  44952
  Copyright terms: Public domain W3C validator