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

Theorem nfsbv 2328
Description: If 𝑧 is not free in 𝜑, then it is not free in [𝑦 / 𝑥]𝜑 when 𝑧 is disjoint from both 𝑥 and 𝑦. Version of nfsb 2529 with an additional disjoint variable condition on 𝑥, 𝑧 but not requiring ax-13 2374. (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 2192 . . 3 (𝜑 → ∀𝑧𝜑)
32hbsbw 2173 . 2 ([𝑦 / 𝑥]𝜑 → ∀𝑧[𝑦 / 𝑥]𝜑)
43nf5i 2146 1 𝑧[𝑦 / 𝑥]𝜑
Colors of variables: wff setvar class
Syntax hints:  wnf 1790  [wsb 2071
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-10 2141  ax-11 2158  ax-12 2175
This theorem depends on definitions:  df-bi 206  df-ex 1787  df-nf 1791  df-sb 2072
This theorem is referenced by:  hbsbwOLD  2330  sbco2v  2331  2sb8ev  2356  sb8euv  2601  2mo  2652  nfcriiOLD  2902  cbvralfwOLD  3368  cbvreuw  3374  cbvrabw  3423  cbvrabcsfw  3881  cbvopab1  5154  cbvmptf  5188  ralxpf  5753  cbviotaw  6396  cbvriotaw  7235  dfoprab4f  7887  mo5f  30831  ax11-pm2  35013  dfich2  44877  ichbi12i  44879
  Copyright terms: Public domain W3C validator