Metamath Proof Explorer

Theorem dmfex

Description: If a mapping is a set, its domain is a set. (Contributed by NM, 27-Aug-2006) (Proof shortened by Andrew Salmon, 17-Sep-2011)

Ref Expression
Assertion dmfex 
|- ( ( F e. C /\ F : A --> B ) -> A e. _V )

Proof

Step Hyp Ref Expression
1 fdm 
 |-  ( F : A --> B -> dom F = A )
2 dmexg 
 |-  ( F e. C -> dom F e. _V )
3 eleq1 
 |-  ( dom F = A -> ( dom F e. _V <-> A e. _V ) )
4 2 3 imbitrid 
 |-  ( dom F = A -> ( F e. C -> A e. _V ) )
5 1 4 syl 
 |-  ( F : A --> B -> ( F e. C -> A e. _V ) )
6 5 impcom 
 |-  ( ( F e. C /\ F : A --> B ) -> A e. _V )