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 )