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

Theorem sb2 1694
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 1443 . 2 (∀𝑥(𝑥 = 𝑦𝜑) → (𝑥 = 𝑦𝜑))
2 equs4 1657 . 2 (∀𝑥(𝑥 = 𝑦𝜑) → ∃𝑥(𝑥 = 𝑦𝜑))
3 df-sb 1690 . 2 ([𝑦 / 𝑥]𝜑 ↔ ((𝑥 = 𝑦𝜑) ∧ ∃𝑥(𝑥 = 𝑦𝜑)))
41, 2, 3sylanbrc 408 1 (∀𝑥(𝑥 = 𝑦𝜑) → [𝑦 / 𝑥]𝜑)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102  wal 1285  wex 1424  [wsb 1689
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1379  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-4 1443  ax-i9 1466  ax-ial 1470
This theorem depends on definitions:  df-bi 115  df-sb 1690
This theorem is referenced by:  stdpc4  1702  equsb1  1712  equsb2  1713  sbiedh  1714  sb6f  1728  hbsb2a  1731  hbsb2e  1732  sbcof2  1735  sb3  1756  sb4b  1759  sb4bor  1760  hbsb2  1761  nfsb2or  1762  sb6rf  1778  sbi1v  1816  sbalyz  1920  iota4  4966
  Copyright terms: Public domain W3C validator