This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 elissetv ⊢ A ∈ x | φ → ∃ y y = A
2 exsimpl ⊢ ∃ x x = A ∧ φ → ∃ x x = A
3 iseqsetv-cleq ⊢ ∃ x x = A ↔ ∃ y y = A
4 2 3 sylib ⊢ ∃ x x = A ∧ φ → ∃ y y = A
5 eleq1 ⊢ y = A → y ∈ x | φ ↔ A ∈ x | φ
6 df-clab ⊢ y ∈ x | φ ↔ y x φ
7 sb5 ⊢ y x φ ↔ ∃ x x = y ∧ φ
8 6 7 bitri ⊢ y ∈ x | φ ↔ ∃ x x = y ∧ φ
9 eqeq2 ⊢ y = A → x = y ↔ x = A
10 9 anbi1d ⊢ y = A → x = y ∧ φ ↔ x = A ∧ φ
11 10 exbidv ⊢ y = A → ∃ x x = y ∧ φ ↔ ∃ x x = A ∧ φ
12 8 11 bitrid ⊢ y = A → y ∈ x | φ ↔ ∃ x x = A ∧ φ
13 5 12 bitr3d ⊢ y = A → A ∈ x | φ ↔ ∃ x x = A ∧ φ
14 13 exlimiv ⊢ ∃ y y = A → A ∈ x | φ ↔ ∃ x x = A ∧ φ
15 1 4 14 pm5.21nii ⊢ A ∈ x | φ ↔ ∃ x x = A ∧ φ