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 φ