Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  fvmptss Unicode version

Theorem fvmptss 5609
 Description: If all the values of the mapping are subsets of a class , then so is any evaluation of the mapping, even if is not in the base set . (Contributed by Mario Carneiro, 13-Feb-2015.)
Hypothesis
Ref Expression
fvmpt2.1
Assertion
Ref Expression
fvmptss
Distinct variable groups:   ,   ,
Allowed substitution hints:   ()   ()   ()

Proof of Theorem fvmptss
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 fvmpt2.1 . . . . 5
21dmmptss 5169 . . . 4
32sseli 3176 . . 3
4 fveq2 5525 . . . . . . 7
54sseq1d 3205 . . . . . 6
65imbi2d 307 . . . . 5
7 nfcv 2419 . . . . . 6
8 nfra1 2593 . . . . . . 7
9 nfmpt1 4109 . . . . . . . . . 10
101, 9nfcxfr 2416 . . . . . . . . 9
1110, 7nffv 5532 . . . . . . . 8
12 nfcv 2419 . . . . . . . 8
1311, 12nfss 3173 . . . . . . 7
148, 13nfim 1769 . . . . . 6
15 fveq2 5525 . . . . . . . 8
1615sseq1d 3205 . . . . . . 7
1716imbi2d 307 . . . . . 6
181dmmpt 5168 . . . . . . . . . . 11
1918rabeq2i 2785 . . . . . . . . . 10
201fvmpt2 5608 . . . . . . . . . . 11
21 eqimss 3230 . . . . . . . . . . 11
2220, 21syl 15 . . . . . . . . . 10
2319, 22sylbi 187 . . . . . . . . 9
24 ndmfv 5552 . . . . . . . . . 10
25 0ss 3483 . . . . . . . . . . 11
2625a1i 10 . . . . . . . . . 10
2724, 26eqsstrd 3212 . . . . . . . . 9
2823, 27pm2.61i 156 . . . . . . . 8
29 rsp 2603 . . . . . . . . 9
3029impcom 419 . . . . . . . 8
3128, 30syl5ss 3190 . . . . . . 7
3231ex 423 . . . . . 6
337, 14, 17, 32vtoclgaf 2848 . . . . 5
346, 33vtoclga 2849 . . . 4
3534impcom 419 . . 3
363, 35sylan2 460 . 2
37 ndmfv 5552 . . . 4