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 5158 | . 2 ⊢ Ⅎ𝑥(𝑥 ∈ 𝐴 ↦ 𝐵) | |
2 | nfcv 2904 | . 2 ⊢ Ⅎ𝑥𝐶 | |
3 | 1, 2 | nffv 6732 | 1 ⊢ Ⅎ𝑥((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝐶) |
Colors of variables: wff setvar class |
Syntax hints: Ⅎwnfc 2884 ↦ cmpt 5140 ‘cfv 6385 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2016 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2158 ax-12 2175 ax-ext 2708 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 848 df-3an 1091 df-tru 1546 df-fal 1556 df-ex 1788 df-nf 1792 df-sb 2071 df-clab 2715 df-cleq 2729 df-clel 2816 df-nfc 2886 df-ral 3066 df-rex 3067 df-rab 3070 df-v 3415 df-dif 3874 df-un 3876 df-in 3878 df-ss 3888 df-nul 4243 df-if 4445 df-sn 4547 df-pr 4549 df-op 4553 df-uni 4825 df-br 5059 df-opab 5121 df-mpt 5141 df-iota 6343 df-fv 6393 |
This theorem is referenced by: fvmptt 6843 fmptco 6949 offval2f 7488 offval2 7493 ofrfval2 7494 mptelixpg 8621 dom2lem 8673 cantnflem1 9309 acni2 9665 axcc2 10056 seqof2 13639 rlim2 15062 ello1mpt 15087 o1compt 15153 sumfc 15278 fsum 15289 fsumf1o 15292 sumss 15293 fsumcvg2 15296 fsumadd 15309 isummulc2 15331 fsummulc2 15353 fsumrelem 15376 isumshft 15408 zprod 15504 fprod 15508 prodfc 15512 fprodf1o 15513 fprodmul 15527 fproddiv 15528 iserodd 16393 prdsbas3 16991 prdsdsval2 16994 invfuc 17488 yonedalem4b 17789 gsumdixp 19632 evlslem4 21039 elptr2 22476 ptunimpt 22497 ptcldmpt 22516 ptclsg 22517 txcnp 22522 ptcnplem 22523 cnmpt1t 22567 cnmptk2 22588 flfcnp2 22909 voliun 24456 mbfeqalem1 24543 mbfpos 24553 mbfposb 24555 mbfsup 24566 mbfinf 24567 mbflim 24570 i1fposd 24610 isibl2 24669 itgmpt 24685 itgeqa 24716 itggt0 24746 itgcn 24747 limcmpt 24785 lhop2 24917 itgsubstlem 24950 itgsubst 24951 elplyd 25101 coeeq2 25141 dgrle 25142 ulmss 25294 itgulm2 25306 leibpi 25830 rlimcnp 25853 o1cxp 25862 lgamgulmlem2 25917 lgamgulmlem6 25921 fmptcof2 30719 itggt0cn 35589 elrfirn2 40229 eq0rabdioph 40309 monotoddzz 40476 aomclem8 40597 fmuldfeq 42807 vonioo 43903 |
Copyright terms: Public domain | W3C validator |