![]() |
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 5256 | . 2 ⊢ Ⅎ𝑥(𝑥 ∈ 𝐴 ↦ 𝐵) | |
2 | nfcv 2899 | . 2 ⊢ Ⅎ𝑥𝐶 | |
3 | 1, 2 | nffv 6907 | 1 ⊢ Ⅎ𝑥((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝐶) |
Colors of variables: wff setvar class |
Syntax hints: Ⅎwnfc 2879 ↦ cmpt 5231 ‘cfv 6548 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-10 2130 ax-11 2147 ax-12 2167 ax-ext 2699 |
This theorem depends on definitions: df-bi 206 df-an 396 df-or 847 df-3an 1087 df-tru 1537 df-fal 1547 df-ex 1775 df-nf 1779 df-sb 2061 df-clab 2706 df-cleq 2720 df-clel 2806 df-nfc 2881 df-ral 3059 df-rex 3068 df-rab 3430 df-v 3473 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-nul 4324 df-if 4530 df-sn 4630 df-pr 4632 df-op 4636 df-uni 4909 df-br 5149 df-opab 5211 df-mpt 5232 df-iota 6500 df-fv 6556 |
This theorem is referenced by: fvmptt 7025 fmptco 7138 offval2f 7700 offval2 7705 ofrfval2 7706 mptelixpg 8953 dom2lem 9012 cantnflem1 9712 acni2 10069 axcc2 10460 seqof2 14057 rlim2 15472 ello1mpt 15497 o1compt 15563 sumfc 15687 fsum 15698 fsumf1o 15701 sumss 15702 fsumcvg2 15705 fsumadd 15718 isummulc2 15740 fsummulc2 15762 fsumrelem 15785 isumshft 15817 zprod 15913 fprod 15917 prodfc 15921 fprodf1o 15922 fprodmul 15936 fproddiv 15937 iserodd 16803 prdsbas3 17462 prdsdsval2 17465 invfuc 17965 yonedalem4b 18267 gsumdixp 20254 evlslem4 22019 elptr2 23477 ptunimpt 23498 ptcldmpt 23517 ptclsg 23518 txcnp 23523 ptcnplem 23524 cnmpt1t 23568 cnmptk2 23589 flfcnp2 23910 voliun 25482 mbfeqalem1 25569 mbfpos 25579 mbfposb 25581 mbfsup 25592 mbfinf 25593 mbflim 25596 i1fposd 25636 isibl2 25695 itgmpt 25711 itgeqa 25742 itggt0 25772 itgcn 25773 limcmpt 25811 lhop2 25947 itgsubstlem 25982 itgsubst 25983 elplyd 26135 coeeq2 26175 dgrle 26176 ulmss 26332 itgulm2 26344 leibpi 26873 rlimcnp 26896 o1cxp 26906 lgamgulmlem2 26961 lgamgulmlem6 26965 fmptcof2 32442 itggt0cn 37163 elrfirn2 42116 eq0rabdioph 42196 monotoddzz 42364 aomclem8 42485 fmuldfeq 44971 vonioo 46070 |
Copyright terms: Public domain | W3C validator |