Metamath Proof Explorer


Theorem ssd

Description: A sufficient condition for a subclass relationship. (Contributed by Glauco Siliprandi, 3-Jan-2021)

Ref Expression
Hypothesis ssd.1 φxAxB
Assertion ssd φAB

Proof

Step Hyp Ref Expression
1 ssd.1 φxAxB
2 nfv xφ
3 2 1 ssdf φAB