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)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | vtoclegft | ⊢ ( ( 𝐴 ∈ 𝐵 ∧ Ⅎ 𝑥 𝜑 ∧ ∀ 𝑥 ( 𝑥 = 𝐴 → 𝜑 ) ) → 𝜑 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | elisset | ⊢ ( 𝐴 ∈ 𝐵 → ∃ 𝑥 𝑥 = 𝐴 ) | |
| 2 | exim | ⊢ ( ∀ 𝑥 ( 𝑥 = 𝐴 → 𝜑 ) → ( ∃ 𝑥 𝑥 = 𝐴 → ∃ 𝑥 𝜑 ) ) | |
| 3 | 1 2 | mpan9 | ⊢ ( ( 𝐴 ∈ 𝐵 ∧ ∀ 𝑥 ( 𝑥 = 𝐴 → 𝜑 ) ) → ∃ 𝑥 𝜑 ) |
| 4 | 3 | 3adant2 | ⊢ ( ( 𝐴 ∈ 𝐵 ∧ Ⅎ 𝑥 𝜑 ∧ ∀ 𝑥 ( 𝑥 = 𝐴 → 𝜑 ) ) → ∃ 𝑥 𝜑 ) |
| 5 | 19.9t | ⊢ ( Ⅎ 𝑥 𝜑 → ( ∃ 𝑥 𝜑 ↔ 𝜑 ) ) | |
| 6 | 5 | 3ad2ant2 | ⊢ ( ( 𝐴 ∈ 𝐵 ∧ Ⅎ 𝑥 𝜑 ∧ ∀ 𝑥 ( 𝑥 = 𝐴 → 𝜑 ) ) → ( ∃ 𝑥 𝜑 ↔ 𝜑 ) ) |
| 7 | 4 6 | mpbid | ⊢ ( ( 𝐴 ∈ 𝐵 ∧ Ⅎ 𝑥 𝜑 ∧ ∀ 𝑥 ( 𝑥 = 𝐴 → 𝜑 ) ) → 𝜑 ) |