Metamath Proof Explorer

Theorem ssdmral

Description: Subclass of a domain. (Contributed by Peter Mazsa, 15-Sep-2018)

Ref Expression
Assertion ssdmral 
|- ( A C_ dom R <-> A. x e. A E. y x R y )

Proof

Step Hyp Ref Expression
1 dfss3 
 |-  ( A C_ dom R <-> A. x e. A x e. dom R )
2 eldmg 
 |-  ( x e. _V -> ( x e. dom R <-> E. y x R y ) )
3 2 elv 
 |-  ( x e. dom R <-> E. y x R y )
4 3 ralbii 
 |-  ( A. x e. A x e. dom R <-> A. x e. A E. y x R y )
5 1 4 bitri 
 |-  ( A C_ dom R <-> A. x e. A E. y x R y )