Metamath Proof Explorer

Theorem clelab

Description: Membership of a class variable in a class abstraction. (Contributed by NM, 23-Dec-1993) (Proof shortened by Wolf Lammen, 16-Nov-2019) Avoid ax-11 , see sbc5ALT for more details. (Revised by SN, 2-Sep-2024)

Ref Expression
Assertion clelab ⊢ A ∈ x | φ ↔ ∃ x x = A ∧ φ

Proof

Step Hyp Ref Expression
1 elisset ⊢ A ∈ x | φ → ∃ y y = A
2 exsimpl ⊢ ∃ x x = A ∧ φ → ∃ x x = A
3 eqeq1 ⊢ x = y → x = A ↔ y = A
4 3 cbvexvw ⊢ ∃ x x = A ↔ ∃ y y = A
5 2 4 sylib ⊢ ∃ x x = A ∧ φ → ∃ y y = A
6 df-clab ⊢ y ∈ x | φ ↔ y x φ
7 sb5 ⊢ y x φ ↔ ∃ x x = y ∧ φ
8 6 7 bitri ⊢ y ∈ x | φ ↔ ∃ x x = y ∧ φ
9 eleq1 ⊢ y = A → y ∈ x | φ ↔ A ∈ x | φ
10 eqeq2 ⊢ y = A → x = y ↔ x = A
11 10 anbi1d ⊢ y = A → x = y ∧ φ ↔ x = A ∧ φ
12 11 exbidv ⊢ y = A → ∃ x x = y ∧ φ ↔ ∃ x x = A ∧ φ
13 9 12 bibi12d ⊢ y = A → y ∈ x | φ ↔ ∃ x x = y ∧ φ ↔ A ∈ x | φ ↔ ∃ x x = A ∧ φ
14 8 13 mpbii ⊢ y = A → A ∈ x | φ ↔ ∃ x x = A ∧ φ
15 14 exlimiv ⊢ ∃ y y = A → A ∈ x | φ ↔ ∃ x x = A ∧ φ
16 1 5 15 pm5.21nii ⊢ A ∈ x | φ ↔ ∃ x x = A ∧ φ