Metamath Proof Explorer

Theorem dfss3

Description: Alternate definition of subclass relationship. (Contributed by NM, 14-Oct-1999)

Ref Expression
Assertion dfss3 
|- ( A C_ B <-> A. x e. A x e. B )

Proof

Step Hyp Ref Expression
1 dfss2 
 |-  ( A C_ B <-> A. x ( x e. A -> x e. B ) )
2 df-ral 
 |-  ( A. x e. A x e. B <-> A. x ( x e. A -> x e. B ) )
3 1 2 bitr4i 
 |-  ( A C_ B <-> A. x e. A x e. B )