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 φ