**Description:** An equality theorem for substitution. (Contributed by NM, 14-May-1993)

Ref | Expression | ||
---|---|---|---|

Assertion | sbequ12 | ⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ [ 𝑦 / 𝑥 ] 𝜑 ) ) |

Step | Hyp | Ref | Expression |
---|---|---|---|

1 | sbequ1 | ⊢ ( 𝑥 = 𝑦 → ( 𝜑 → [ 𝑦 / 𝑥 ] 𝜑 ) ) | |

2 | sbequ2 | ⊢ ( 𝑥 = 𝑦 → ( [ 𝑦 / 𝑥 ] 𝜑 → 𝜑 ) ) | |

3 | 1 2 | impbid | ⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ [ 𝑦 / 𝑥 ] 𝜑 ) ) |