New Foundations Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  NFE Home  >  Th. List  >  sb2 GIF version

Theorem sb2 2023
 Description: One direction of a simplified definition of substitution. (Contributed by NM, 5-Aug-1993.)
Assertion
Ref Expression
sb2 (x(x = yφ) → [y / x]φ)

Proof of Theorem sb2
StepHypRef Expression
1 sp 1747 . 2 (x(x = yφ) → (x = yφ))
2 equs4 1959 . 2 (x(x = yφ) → x(x = y φ))
3 df-sb 1649 . 2 ([y / x]φ ↔ ((x = yφ) x(x = y φ)))
41, 2, 3sylanbrc 645 1 (x(x = yφ) → [y / x]φ)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 358  ∀wal 1540  ∃wex 1541  [wsb 1648 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925 This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649 This theorem is referenced by:  stdpc4  2024  equsb1  2034  equsb2  2035  sbied  2036  sb6f  2039  hbsb2a  2041  hbsb2e  2042  sb3  2052  sb4b  2054  dfsb2  2055  hbsb2  2057  sbn  2062  sbi1  2063  sb6rf  2091  sbal1  2126  iota4  4357
 Copyright terms: Public domain W3C validator