**Description:** An equality theorem for substitution. (Contributed by NM, 16-May-1993)
Revise df-sb . (Revised by BJ, 22-Dec-2020)

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

Assertion | sbequ1 | ⊢ ( 𝑥 = 𝑡 → ( 𝜑 → [ 𝑡 / 𝑥 ] 𝜑 ) ) |

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

1 | equeucl | ⊢ ( 𝑥 = 𝑡 → ( 𝑦 = 𝑡 → 𝑥 = 𝑦 ) ) | |

2 | ax12v | ⊢ ( 𝑥 = 𝑦 → ( 𝜑 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ) ) | |

3 | 1 2 | syl6 | ⊢ ( 𝑥 = 𝑡 → ( 𝑦 = 𝑡 → ( 𝜑 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ) ) ) |

4 | 3 | com23 | ⊢ ( 𝑥 = 𝑡 → ( 𝜑 → ( 𝑦 = 𝑡 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ) ) ) |

5 | 4 | alrimdv | ⊢ ( 𝑥 = 𝑡 → ( 𝜑 → ∀ 𝑦 ( 𝑦 = 𝑡 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ) ) ) |

6 | df-sb | ⊢ ( [ 𝑡 / 𝑥 ] 𝜑 ↔ ∀ 𝑦 ( 𝑦 = 𝑡 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ) ) | |

7 | 5 6 | syl6ibr | ⊢ ( 𝑥 = 𝑡 → ( 𝜑 → [ 𝑡 / 𝑥 ] 𝜑 ) ) |