Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > nffvmpt1 | Structured version Visualization version GIF version |
Description: Bound-variable hypothesis builder for mapping, special case. (Contributed by Mario Carneiro, 25-Dec-2016.) |
Ref | Expression |
---|---|
nffvmpt1 | ⊢ Ⅎ𝑥((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝐶) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfmpt1 5155 | . 2 ⊢ Ⅎ𝑥(𝑥 ∈ 𝐴 ↦ 𝐵) | |
2 | nfcv 2974 | . 2 ⊢ Ⅎ𝑥𝐶 | |
3 | 1, 2 | nffv 6673 | 1 ⊢ Ⅎ𝑥((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝐶) |
Colors of variables: wff setvar class |
Syntax hints: Ⅎwnfc 2958 ↦ cmpt 5137 ‘cfv 6348 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2151 ax-12 2167 ax-ext 2790 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-3an 1081 df-tru 1531 df-ex 1772 df-nf 1776 df-sb 2061 df-clab 2797 df-cleq 2811 df-clel 2890 df-nfc 2960 df-ral 3140 df-rex 3141 df-rab 3144 df-v 3494 df-dif 3936 df-un 3938 df-in 3940 df-ss 3949 df-nul 4289 df-if 4464 df-sn 4558 df-pr 4560 df-op 4564 df-uni 4831 df-br 5058 df-opab 5120 df-mpt 5138 df-iota 6307 df-fv 6356 |
This theorem is referenced by: fvmptt 6780 fmptco 6883 offval2f 7410 offval2 7415 ofrfval2 7416 mptelixpg 8487 dom2lem 8537 cantnflem1 9140 acni2 9460 axcc2 9847 seqof2 13416 rlim2 14841 ello1mpt 14866 o1compt 14932 sumfc 15054 fsum 15065 fsumf1o 15068 sumss 15069 fsumcvg2 15072 fsumadd 15084 isummulc2 15105 fsummulc2 15127 fsumrelem 15150 isumshft 15182 zprod 15279 fprod 15283 prodfc 15287 fprodf1o 15288 fprodmul 15302 fproddiv 15303 iserodd 16160 prdsbas3 16742 prdsdsval2 16745 invfuc 17232 yonedalem4b 17514 gsumdixp 19288 evlslem4 20216 elptr2 22110 ptunimpt 22131 ptcldmpt 22150 ptclsg 22151 txcnp 22156 ptcnplem 22157 cnmpt1t 22201 cnmptk2 22222 flfcnp2 22543 voliun 24082 mbfeqalem1 24169 mbfpos 24179 mbfposb 24181 mbfsup 24192 mbfinf 24193 mbflim 24196 i1fposd 24235 isibl2 24294 itgmpt 24310 itgeqa 24341 itggt0 24369 itgcn 24370 limcmpt 24408 lhop2 24539 itgsubstlem 24572 itgsubst 24573 elplyd 24719 coeeq2 24759 dgrle 24760 ulmss 24912 itgulm2 24924 leibpi 25447 rlimcnp 25470 o1cxp 25479 lgamgulmlem2 25534 lgamgulmlem6 25538 fmptcof2 30330 itggt0cn 34845 elrfirn2 39171 eq0rabdioph 39251 monotoddzz 39418 aomclem8 39539 fmuldfeq 41740 vonioo 42841 |
Copyright terms: Public domain | W3C validator |