Metamath Proof Explorer


Theorem dmss

Description: Subset theorem for domain. (Contributed by NM, 11-Aug-1994)

Ref Expression
Assertion dmss
|- ( A C_ B -> dom A C_ dom B )

Proof

Step Hyp Ref Expression
1 ssel
 |-  ( A C_ B -> ( <. x , y >. e. A -> <. x , y >. e. B ) )
2 1 eximdv
 |-  ( A C_ B -> ( E. y <. x , y >. e. A -> E. y <. x , y >. e. B ) )
3 vex
 |-  x e. _V
4 3 eldm2
 |-  ( x e. dom A <-> E. y <. x , y >. e. A )
5 3 eldm2
 |-  ( x e. dom B <-> E. y <. x , y >. e. B )
6 2 4 5 3imtr4g
 |-  ( A C_ B -> ( x e. dom A -> x e. dom B ) )
7 6 ssrdv
 |-  ( A C_ B -> dom A C_ dom B )