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 ( ( 𝐹𝐶𝐹 : 𝐴𝐵 ) → 𝐴 ∈ V )

Proof

Step Hyp Ref Expression
1 fdm ( 𝐹 : 𝐴𝐵 → dom 𝐹 = 𝐴 )
2 dmexg ( 𝐹𝐶 → dom 𝐹 ∈ V )
3 eleq1 ( dom 𝐹 = 𝐴 → ( dom 𝐹 ∈ V ↔ 𝐴 ∈ V ) )
4 2 3 syl5ib ( dom 𝐹 = 𝐴 → ( 𝐹𝐶𝐴 ∈ V ) )
5 1 4 syl ( 𝐹 : 𝐴𝐵 → ( 𝐹𝐶𝐴 ∈ V ) )
6 5 impcom ( ( 𝐹𝐶𝐹 : 𝐴𝐵 ) → 𝐴 ∈ V )