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

Theorem nfsbv 2351
 Description: If 𝑧 is not free in 𝜑, it is not free in [𝑦 / 𝑥]𝜑 when 𝑧 is distinct from 𝑥 and 𝑦. Version of nfsb 2567 requiring more disjoint variables, but fewer axioms. (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.)
Hypothesis
Ref Expression
nfsbv.nf 𝑧𝜑
Assertion
Ref Expression
nfsbv 𝑧[𝑦 / 𝑥]𝜑
Distinct variable groups:   𝑥,𝑧   𝑦,𝑧
Allowed substitution hints:   𝜑(𝑥,𝑦,𝑧)

Proof of Theorem nfsbv
Dummy variable 𝑤 is distinct from all other variables.
StepHypRef Expression
1 df-sb 2071 . 2 ([𝑦 / 𝑥]𝜑 ↔ ∀𝑤(𝑤 = 𝑦 → ∀𝑥(𝑥 = 𝑤𝜑)))
2 nfv 1916 . . . 4 𝑧 𝑤 = 𝑦
3 nfv 1916 . . . . . 6 𝑧 𝑥 = 𝑤
4 nfsbv.nf . . . . . 6 𝑧𝜑
53, 4nfim 1898 . . . . 5 𝑧(𝑥 = 𝑤𝜑)
65nfal 2344 . . . 4 𝑧𝑥(𝑥 = 𝑤𝜑)
72, 6nfim 1898 . . 3 𝑧(𝑤 = 𝑦 → ∀𝑥(𝑥 = 𝑤𝜑))
87nfal 2344 . 2 𝑧𝑤(𝑤 = 𝑦 → ∀𝑥(𝑥 = 𝑤𝜑))
91, 8nfxfr 1854 1 𝑧[𝑦 / 𝑥]𝜑
 Colors of variables: wff setvar class Syntax hints:   → wi 4  ∀wal 1536  Ⅎwnf 1785  [wsb 2070 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-10 2146  ax-11 2162  ax-12 2179 This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-nf 1786  df-sb 2071 This theorem is referenced by:  hbsbwOLD  2353  sbco2v  2354  2sb8ev  2377  sb8euv  2686  2mo  2736  nfcriiOLD  2975  cbvralfwOLD  3421  cbvreuw  3427  cbvrabw  3475  cbvrabcsfw  3907  cbvopab1  5125  cbvmptf  5151  ralxpf  5704  cbviotaw  6309  cbvriotaw  7116  dfoprab4f  7749  mo5f  30266  ax11-pm2  34222  dfich2  43906  ichbi12i  43908
 Copyright terms: Public domain W3C validator