Description: A representation of explicit substitution of a class for a variable, inferred from an implicit substitution hypothesis. (Contributed by NM, 18-Aug-1993) Avoid ax-12 . (Revised by SN, 8-Sep-2024)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | ceqsalv.1 | ⊢ 𝐴 ∈ V | |
| ceqsalv.2 | ⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) ) | ||
| Assertion | ceqsalv | ⊢ ( ∀ 𝑥 ( 𝑥 = 𝐴 → 𝜑 ) ↔ 𝜓 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ceqsalv.1 | ⊢ 𝐴 ∈ V | |
| 2 | ceqsalv.2 | ⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) ) | |
| 3 | 2 | pm5.74i | ⊢ ( ( 𝑥 = 𝐴 → 𝜑 ) ↔ ( 𝑥 = 𝐴 → 𝜓 ) ) |
| 4 | 3 | albii | ⊢ ( ∀ 𝑥 ( 𝑥 = 𝐴 → 𝜑 ) ↔ ∀ 𝑥 ( 𝑥 = 𝐴 → 𝜓 ) ) |
| 5 | 19.23v | ⊢ ( ∀ 𝑥 ( 𝑥 = 𝐴 → 𝜓 ) ↔ ( ∃ 𝑥 𝑥 = 𝐴 → 𝜓 ) ) | |
| 6 | 1 | isseti | ⊢ ∃ 𝑥 𝑥 = 𝐴 |
| 7 | pm5.5 | ⊢ ( ∃ 𝑥 𝑥 = 𝐴 → ( ( ∃ 𝑥 𝑥 = 𝐴 → 𝜓 ) ↔ 𝜓 ) ) | |
| 8 | 6 7 | ax-mp | ⊢ ( ( ∃ 𝑥 𝑥 = 𝐴 → 𝜓 ) ↔ 𝜓 ) |
| 9 | 4 5 8 | 3bitri | ⊢ ( ∀ 𝑥 ( 𝑥 = 𝐴 → 𝜑 ) ↔ 𝜓 ) |