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 5156 | . 2 ⊢ Ⅎ𝑥(𝑥 ∈ 𝐴 ↦ 𝐵) | |
2 | nfcv 2977 | . 2 ⊢ Ⅎ𝑥𝐶 | |
3 | 1, 2 | nffv 6674 | 1 ⊢ Ⅎ𝑥((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝐶) |
Colors of variables: wff setvar class |
Syntax hints: Ⅎwnfc 2961 ↦ cmpt 5138 ‘cfv 6349 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1907 ax-6 1966 ax-7 2011 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2157 ax-12 2173 ax-ext 2793 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3an 1085 df-tru 1536 df-ex 1777 df-nf 1781 df-sb 2066 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-ral 3143 df-rex 3144 df-rab 3147 df-v 3496 df-dif 3938 df-un 3940 df-in 3942 df-ss 3951 df-nul 4291 df-if 4467 df-sn 4561 df-pr 4563 df-op 4567 df-uni 4832 df-br 5059 df-opab 5121 df-mpt 5139 df-iota 6308 df-fv 6357 |
This theorem is referenced by: fvmptt 6782 fmptco 6885 offval2f 7415 offval2 7420 ofrfval2 7421 mptelixpg 8493 dom2lem 8543 cantnflem1 9146 acni2 9466 axcc2 9853 seqof2 13422 rlim2 14847 ello1mpt 14872 o1compt 14938 sumfc 15060 fsum 15071 fsumf1o 15074 sumss 15075 fsumcvg2 15078 fsumadd 15090 isummulc2 15111 fsummulc2 15133 fsumrelem 15156 isumshft 15188 zprod 15285 fprod 15289 prodfc 15293 fprodf1o 15294 fprodmul 15308 fproddiv 15309 iserodd 16166 prdsbas3 16748 prdsdsval2 16751 invfuc 17238 yonedalem4b 17520 gsumdixp 19353 evlslem4 20282 elptr2 22176 ptunimpt 22197 ptcldmpt 22216 ptclsg 22217 txcnp 22222 ptcnplem 22223 cnmpt1t 22267 cnmptk2 22288 flfcnp2 22609 voliun 24149 mbfeqalem1 24236 mbfpos 24246 mbfposb 24248 mbfsup 24259 mbfinf 24260 mbflim 24263 i1fposd 24302 isibl2 24361 itgmpt 24377 itgeqa 24408 itggt0 24436 itgcn 24437 limcmpt 24475 lhop2 24606 itgsubstlem 24639 itgsubst 24640 elplyd 24786 coeeq2 24826 dgrle 24827 ulmss 24979 itgulm2 24991 leibpi 25514 rlimcnp 25537 o1cxp 25546 lgamgulmlem2 25601 lgamgulmlem6 25605 fmptcof2 30396 itggt0cn 34958 elrfirn2 39286 eq0rabdioph 39366 monotoddzz 39533 aomclem8 39654 fmuldfeq 41857 vonioo 42958 |
Copyright terms: Public domain | W3C validator |