Metamath Proof Explorer

Theorem vtoclegft

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 ⊢ A ∈ B ∧ Ⅎ x φ ∧ ∀ x x = A → φ → φ

Proof

Step Hyp Ref Expression
1 biidd ⊢ x = A → φ ↔ φ
2 1 ax-gen ⊢ ∀ x x = A → φ ↔ φ
3 ceqsalt ⊢ Ⅎ x φ ∧ ∀ x x = A → φ ↔ φ ∧ A ∈ B → ∀ x x = A → φ ↔ φ
4 2 3 mp3an2 ⊢ Ⅎ x φ ∧ A ∈ B → ∀ x x = A → φ ↔ φ
5 4 ancoms ⊢ A ∈ B ∧ Ⅎ x φ → ∀ x x = A → φ ↔ φ
6 5 biimpd ⊢ A ∈ B ∧ Ⅎ x φ → ∀ x x = A → φ → φ
7 6 3impia ⊢ A ∈ B ∧ Ⅎ x φ ∧ ∀ x x = A → φ → φ