Metamath Proof Explorer

Theorem elabgt

Description: Membership in a class abstraction, using implicit substitution. (Closed theorem version of elabg .) (Contributed by NM, 7-Nov-2005) (Proof shortened by Andrew Salmon, 8-Jun-2011)

Ref Expression
Assertion elabgt ⊢ A ∈ B ∧ ∀ x x = A → φ ↔ ψ → A ∈ x | φ ↔ ψ

Proof

Step Hyp Ref Expression
1 nfcv ⊢ Ⅎ _ x A
2 nfab1 ⊢ Ⅎ _ x x | φ
3 2 nfel2 ⊢ Ⅎ x A ∈ x | φ
4 nfv ⊢ Ⅎ x ψ
5 3 4 nfbi ⊢ Ⅎ x A ∈ x | φ ↔ ψ
6 pm5.5 ⊢ x = A → x = A → A ∈ x | φ ↔ ψ ↔ A ∈ x | φ ↔ ψ
7 1 5 6 spcgf ⊢ A ∈ B → ∀ x x = A → A ∈ x | φ ↔ ψ → A ∈ x | φ ↔ ψ
8 abid ⊢ x ∈ x | φ ↔ φ
9 eleq1 ⊢ x = A → x ∈ x | φ ↔ A ∈ x | φ
10 8 9 bitr3id ⊢ x = A → φ ↔ A ∈ x | φ
11 10 bibi1d ⊢ x = A → φ ↔ ψ ↔ A ∈ x | φ ↔ ψ
12 11 biimpd ⊢ x = A → φ ↔ ψ → A ∈ x | φ ↔ ψ
13 12 a2i ⊢ x = A → φ ↔ ψ → x = A → A ∈ x | φ ↔ ψ
14 13 alimi ⊢ ∀ x x = A → φ ↔ ψ → ∀ x x = A → A ∈ x | φ ↔ ψ
15 7 14 impel ⊢ A ∈ B ∧ ∀ x x = A → φ ↔ ψ → A ∈ x | φ ↔ ψ