![]() |
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 4971 | . 2 ⊢ Ⅎ𝑥(𝑥 ∈ 𝐴 ↦ 𝐵) | |
2 | nfcv 2970 | . 2 ⊢ Ⅎ𝑥𝐶 | |
3 | 1, 2 | nffv 6444 | 1 ⊢ Ⅎ𝑥((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝐶) |
Colors of variables: wff setvar class |
Syntax hints: Ⅎwnfc 2957 ↦ cmpt 4953 ‘cfv 6124 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1896 ax-4 1910 ax-5 2011 ax-6 2077 ax-7 2114 ax-9 2175 ax-10 2194 ax-11 2209 ax-12 2222 ax-13 2391 ax-ext 2804 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 881 df-3an 1115 df-tru 1662 df-ex 1881 df-nf 1885 df-sb 2070 df-clab 2813 df-cleq 2819 df-clel 2822 df-nfc 2959 df-ral 3123 df-rex 3124 df-rab 3127 df-v 3417 df-dif 3802 df-un 3804 df-in 3806 df-ss 3813 df-nul 4146 df-if 4308 df-sn 4399 df-pr 4401 df-op 4405 df-uni 4660 df-br 4875 df-opab 4937 df-mpt 4954 df-iota 6087 df-fv 6132 |
This theorem is referenced by: fvmptt 6548 fmptco 6647 offval2f 7170 offval2 7175 ofrfval2 7176 mptelixpg 8213 dom2lem 8263 cantnflem1 8864 acni2 9183 axcc2 9575 seqof2 13154 rlim2 14605 ello1mpt 14630 o1compt 14696 sumfc 14818 fsum 14829 fsumf1o 14832 sumss 14833 fsumcvg2 14836 fsumadd 14848 isummulc2 14869 fsummulc2 14891 fsumrelem 14914 isumshft 14946 zprod 15041 fprod 15045 prodfc 15049 fprodf1o 15050 fprodmul 15064 fproddiv 15065 iserodd 15912 prdsbas3 16495 prdsdsval2 16498 invfuc 16987 yonedalem4b 17270 gsumdixp 18964 evlslem4 19869 elptr2 21749 ptunimpt 21770 ptcldmpt 21789 ptclsg 21790 txcnp 21795 ptcnplem 21796 cnmpt1t 21840 cnmptk2 21861 flfcnp2 22182 voliun 23721 mbfeqalem1 23808 mbfpos 23818 mbfposb 23820 mbfsup 23831 mbfinf 23832 mbflim 23835 i1fposd 23874 isibl2 23933 itgmpt 23949 itgeqa 23980 itggt0 24008 itgcn 24009 limcmpt 24047 lhop2 24178 itgsubstlem 24211 itgsubst 24212 elplyd 24358 coeeq2 24398 dgrle 24399 ulmss 24551 itgulm2 24563 leibpi 25083 rlimcnp 25106 o1cxp 25115 lgamgulmlem2 25170 lgamgulmlem6 25174 fmptcof2 30007 itggt0cn 34026 elrfirn2 38104 eq0rabdioph 38185 monotoddzz 38352 aomclem8 38475 fmuldfeq 40611 vonioo 41691 |
Copyright terms: Public domain | W3C validator |