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

Theorem nfsbv 2324
Description: If 𝑧 is not free in 𝜑, then it is not free in [𝑦 / 𝑥]𝜑 when 𝑧 is disjoint from both 𝑥 and 𝑦. Version of nfsb 2526 with an additional disjoint variable condition on 𝑥, 𝑧 but not requiring ax-13 2371. (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 2189 . . 3 (𝜑 → ∀𝑧𝜑)
32hbsbw 2170 . 2 ([𝑦 / 𝑥]𝜑 → ∀𝑧[𝑦 / 𝑥]𝜑)
43nf5i 2143 1 𝑧[𝑦 / 𝑥]𝜑
Colors of variables: wff setvar class
Syntax hints:  wnf 1786  [wsb 2068
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-10 2138  ax-11 2155  ax-12 2172
This theorem depends on definitions:  df-bi 206  df-ex 1783  df-nf 1787  df-sb 2069
This theorem is referenced by:  hbsbwOLD  2326  sbco2v  2327  2sb8ef  2353  sb8euv  2598  2mo  2649  nfcriiOLD  2901  cbvralfwOLD  3307  cbvreuwOLD  3392  cbvrabw  3442  cbvrabcsfw  3904  cbvopab1  5185  cbvmptf  5219  ralxpf  5807  cbviotaw  6460  cbvriotaw  7327  dfoprab4f  7993  mo5f  31459  ax11-pm2  35330  dfich2  45724  ichbi12i  45726
  Copyright terms: Public domain W3C validator