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

Theorem nfsb 2468
Description: If 𝑧 is not free in 𝜑, it is not free in [𝑦 / 𝑥]𝜑 when 𝑦 and 𝑧 are distinct. (Contributed by Mario Carneiro, 11-Aug-2016.)
Hypothesis
Ref Expression
nfsb.1 𝑧𝜑
Assertion
Ref Expression
nfsb 𝑧[𝑦 / 𝑥]𝜑
Distinct variable group:   𝑦,𝑧
Allowed substitution hints:   𝜑(𝑥,𝑦,𝑧)

Proof of Theorem nfsb
StepHypRef Expression
1 axc16nf 2175 . 2 (∀𝑧 𝑧 = 𝑦 → Ⅎ𝑧[𝑦 / 𝑥]𝜑)
2 nfsb.1 . . 3 𝑧𝜑
32nfsb4 2418 . 2 (¬ ∀𝑧 𝑧 = 𝑦 → Ⅎ𝑧[𝑦 / 𝑥]𝜑)
41, 3pm2.61i 176 1 𝑧[𝑦 / 𝑥]𝜑
Colors of variables: wff setvar class
Syntax hints:  wal 1521  wnf 1748  [wsb 1937
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938
This theorem is referenced by:  hbsb  2469  sb10f  2484  2sb8e  2495  sb8eu  2532  2mo  2580  cbvralf  3195  cbvreu  3199  cbvralsv  3212  cbvrexsv  3213  cbvrab  3229  cbvreucsf  3600  cbvrabcsf  3601  cbvopab1  4756  cbvmptf  4781  cbvmpt  4782  ralxpf  5301  cbviota  5894  sb8iota  5896  cbvriota  6661  dfoprab4f  7270  mo5f  29452  ax11-pm2  32948  2sb5nd  39093
  Copyright terms: Public domain W3C validator