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

Theorem sb2 1767
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 1510 . 2 (∀𝑥(𝑥 = 𝑦𝜑) → (𝑥 = 𝑦𝜑))
2 equs4 1725 . 2 (∀𝑥(𝑥 = 𝑦𝜑) → ∃𝑥(𝑥 = 𝑦𝜑))
3 df-sb 1763 . 2 ([𝑦 / 𝑥]𝜑 ↔ ((𝑥 = 𝑦𝜑) ∧ ∃𝑥(𝑥 = 𝑦𝜑)))
41, 2, 3sylanbrc 417 1 (∀𝑥(𝑥 = 𝑦𝜑) → [𝑦 / 𝑥]𝜑)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 104  wal 1351  wex 1492  [wsb 1762
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510  ax-i9 1530  ax-ial 1534
This theorem depends on definitions:  df-bi 117  df-sb 1763
This theorem is referenced by:  stdpc4  1775  equsb1  1785  equsb2  1786  sbiedh  1787  sb6f  1803  hbsb2a  1806  hbsb2e  1807  sbcof2  1810  sb3  1831  sb4b  1834  sb4bor  1835  hbsb2  1836  nfsb2or  1837  sb6rf  1853  sbi1v  1891  sbalyz  1999  iota4  5192
  Copyright terms: Public domain W3C validator