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

Theorem sb2 1723
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 1470 . 2 (∀𝑥(𝑥 = 𝑦𝜑) → (𝑥 = 𝑦𝜑))
2 equs4 1686 . 2 (∀𝑥(𝑥 = 𝑦𝜑) → ∃𝑥(𝑥 = 𝑦𝜑))
3 df-sb 1719 . 2 ([𝑦 / 𝑥]𝜑 ↔ ((𝑥 = 𝑦𝜑) ∧ ∃𝑥(𝑥 = 𝑦𝜑)))
41, 2, 3sylanbrc 411 1 (∀𝑥(𝑥 = 𝑦𝜑) → [𝑦 / 𝑥]𝜑)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  wal 1312  wex 1451  [wsb 1718
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1406  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-4 1470  ax-i9 1493  ax-ial 1497
This theorem depends on definitions:  df-bi 116  df-sb 1719
This theorem is referenced by:  stdpc4  1731  equsb1  1741  equsb2  1742  sbiedh  1743  sb6f  1757  hbsb2a  1760  hbsb2e  1761  sbcof2  1764  sb3  1785  sb4b  1788  sb4bor  1789  hbsb2  1790  nfsb2or  1791  sb6rf  1807  sbi1v  1845  sbalyz  1950  iota4  5074
  Copyright terms: Public domain W3C validator