Metamath Proof Explorer


Theorem bj-clex

Description: Sethood of certain classes. (Contributed by BJ, 2-Apr-2019)

Ref Expression
Assertion bj-clex A V x | x A B V

Proof

Step Hyp Ref Expression
1 imaexg A V A B V
2 bj-snsetex A B V x | x A B V
3 1 2 syl A V x | x A B V