Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  sb2 GIF version

Theorem sb2 1650
 Description: One direction of a simplified definition of substitution. (Contributed by NM, 5-Aug-1993.)
Assertion
Ref Expression
sb2 (∀𝑥(𝑥 = 𝑦𝜑) → [𝑦 / 𝑥]𝜑)

Proof of Theorem sb2
StepHypRef Expression
1 ax-4 1400 . 2 (∀𝑥(𝑥 = 𝑦𝜑) → (𝑥 = 𝑦𝜑))
2 equs4 1613 . 2 (∀𝑥(𝑥 = 𝑦𝜑) → ∃𝑥(𝑥 = 𝑦𝜑))
3 df-sb 1646 . 2 ([𝑦 / 𝑥]𝜑 ↔ ((𝑥 = 𝑦𝜑) ∧ ∃𝑥(𝑥 = 𝑦𝜑)))
41, 2, 3sylanbrc 394 1 (∀𝑥(𝑥 = 𝑦𝜑) → [𝑦 / 𝑥]𝜑)
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 97  ∀wal 1241  ∃wex 1381  [wsb 1645 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1336  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-4 1400  ax-i9 1423  ax-ial 1427 This theorem depends on definitions:  df-bi 110  df-sb 1646 This theorem is referenced by:  stdpc4  1658  equsb1  1668  equsb2  1669  sbiedh  1670  sb6f  1684  hbsb2a  1687  hbsb2e  1688  sbcof2  1691  sb3  1712  sb4b  1715  sb4bor  1716  hbsb2  1717  nfsb2or  1718  sb6rf  1733  sbi1v  1771  sbalyz  1875  iota4  4885
 Copyright terms: Public domain W3C validator