Description: Implicit substitution of a class for a setvar variable. (Closed theorem version of vtoclef .) (Contributed by NM, 7-Nov-2005) (Revised by Mario Carneiro, 11-Oct-2016) (Proof shortened by Wolf Lammen, 26-Jan-2025)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | vtoclegft | ⊢ ( ( 𝐴 ∈ 𝐵 ∧ Ⅎ 𝑥 𝜑 ∧ ∀ 𝑥 ( 𝑥 = 𝐴 → 𝜑 ) ) → 𝜑 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | biidd | ⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜑 ) ) | |
| 2 | 1 | ax-gen | ⊢ ∀ 𝑥 ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜑 ) ) |
| 3 | ceqsalt | ⊢ ( ( Ⅎ 𝑥 𝜑 ∧ ∀ 𝑥 ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜑 ) ) ∧ 𝐴 ∈ 𝐵 ) → ( ∀ 𝑥 ( 𝑥 = 𝐴 → 𝜑 ) ↔ 𝜑 ) ) | |
| 4 | 2 3 | mp3an2 | ⊢ ( ( Ⅎ 𝑥 𝜑 ∧ 𝐴 ∈ 𝐵 ) → ( ∀ 𝑥 ( 𝑥 = 𝐴 → 𝜑 ) ↔ 𝜑 ) ) |
| 5 | 4 | ancoms | ⊢ ( ( 𝐴 ∈ 𝐵 ∧ Ⅎ 𝑥 𝜑 ) → ( ∀ 𝑥 ( 𝑥 = 𝐴 → 𝜑 ) ↔ 𝜑 ) ) |
| 6 | 5 | biimpd | ⊢ ( ( 𝐴 ∈ 𝐵 ∧ Ⅎ 𝑥 𝜑 ) → ( ∀ 𝑥 ( 𝑥 = 𝐴 → 𝜑 ) → 𝜑 ) ) |
| 7 | 6 | 3impia | ⊢ ( ( 𝐴 ∈ 𝐵 ∧ Ⅎ 𝑥 𝜑 ∧ ∀ 𝑥 ( 𝑥 = 𝐴 → 𝜑 ) ) → 𝜑 ) |