Metamath Proof Explorer

Theorem elexd

Description: If a class is a member of another class, then it is a set. Deduction associated with elex . (Contributed by Glauco Siliprandi, 11-Oct-2020)

Ref Expression
Hypothesis elexd.1 φ A V
Assertion elexd φ A V


Step Hyp Ref Expression
1 elexd.1 φ A V
2 elex A V A V
3 1 2 syl φ A V