Metamath Proof Explorer


Theorem fvmptss2

Description: A mapping always evaluates to a subset of the substituted expression in the mapping, even if this is a proper class, or we are out of the domain. (Contributed by Mario Carneiro, 13-Feb-2015)

Ref Expression
Hypotheses fvmptn.1 x = D B = C
fvmptn.2 F = x A B
Assertion fvmptss2 F D C

Proof

Step Hyp Ref Expression
1 fvmptn.1 x = D B = C
2 fvmptn.2 F = x A B
3 1 eleq1d x = D B V C V
4 2 dmmpt dom F = x A | B V
5 3 4 elrab2 D dom F D A C V
6 1 2 fvmptg D A C V F D = C
7 eqimss F D = C F D C
8 6 7 syl D A C V F D C
9 5 8 sylbi D dom F F D C
10 ndmfv ¬ D dom F F D =
11 0ss C
12 10 11 eqsstrdi ¬ D dom F F D C
13 9 12 pm2.61i F D C