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

Theorem nfsbv 2318
Description: If 𝑧 is not free in 𝜑, then it is not free in [𝑦 / 𝑥]𝜑 when 𝑧 is disjoint from both 𝑥 and 𝑦. Version of nfsb 2517 with an additional disjoint variable condition on 𝑥, 𝑧 but not requiring ax-13 2366. (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 2181 . . 3 (𝜑 → ∀𝑧𝜑)
32hbsbw 2162 . 2 ([𝑦 / 𝑥]𝜑 → ∀𝑧[𝑦 / 𝑥]𝜑)
43nf5i 2135 1 𝑧[𝑦 / 𝑥]𝜑
Colors of variables: wff setvar class
Syntax hints:  wnf 1778  [wsb 2060
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-10 2130  ax-11 2147  ax-12 2164
This theorem depends on definitions:  df-bi 206  df-ex 1775  df-nf 1779  df-sb 2061
This theorem is referenced by:  hbsbwOLD  2320  sbco2v  2321  2sb8ef  2347  sb8euv  2588  2mo  2639  nfcriiOLD  2891  cbvralfwOLD  3315  cbvreuwOLD  3407  cbvrabw  3462  cbvrabcsfw  3933  cbvopab1  5217  cbvmptf  5251  ralxpf  5843  cbviotaw  6501  cbvriotaw  7379  dfoprab4f  8052  mo5f  32260  ax11-pm2  36236  dfich2  46711  ichbi12i  46713
  Copyright terms: Public domain W3C validator