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

Theorem fvmptss 5816
 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 5369 . . . 4
32sseli 3346 . . 3
4 fveq2 5731 . . . . . . 7
54sseq1d 3377 . . . . . 6
65imbi2d 309 . . . . 5
7 nfcv 2574 . . . . . 6
8 nfra1 2758 . . . . . . 7
9 nfmpt1 4301 . . . . . . . . . 10
101, 9nfcxfr 2571 . . . . . . . . 9
1110, 7nffv 5738 . . . . . . . 8
12 nfcv 2574 . . . . . . . 8
1311, 12nfss 3343 . . . . . . 7
148, 13nfim 1833 . . . . . 6
15 fveq2 5731 . . . . . . . 8
1615sseq1d 3377 . . . . . . 7
1716imbi2d 309 . . . . . 6
181dmmpt 5368 . . . . . . . . . . 11
1918rabeq2i 2955 . . . . . . . . . 10
201fvmpt2 5815 . . . . . . . . . . 11
21 eqimss 3402 . . . . . . . . . . 11
2220, 21syl 16 . . . . . . . . . 10
2319, 22sylbi 189 . . . . . . . . 9
24 ndmfv 5758 . . . . . . . . . 10
25 0ss 3658 . . . . . . . . . 10
2624, 25syl6eqss 3400 . . . . . . . . 9
2723, 26pm2.61i 159 . . . . . . . 8
28 rsp 2768 . . . . . . . . 9
2928impcom 421 . . . . . . . 8
3027, 29syl5ss 3361 . . . . . . 7
3130ex 425 . . . . . 6
327, 14, 17, 31vtoclgaf 3018 . . . . 5
336, 32vtoclga 3019 . . . 4
3433impcom 421 . . 3
353, 34sylan2 462 . 2
36 ndmfv 5758 . . . 4