Metamath Proof Explorer

Theorem ssexd

Description: A subclass of a set is a set. Deduction form of ssexg . (Contributed by David Moews, 1-May-2017)

Ref Expression
Hypotheses ssexd.1 φ B C
ssexd.2 φ A B
Assertion ssexd φ A V


Step Hyp Ref Expression
1 ssexd.1 φ B C
2 ssexd.2 φ A B
3 ssexg A B B C A V
4 2 1 3 syl2anc φ A V