![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > nfmpt | Structured version Visualization version GIF version |
Description: Bound-variable hypothesis builder for the maps-to notation. (Contributed by NM, 20-Feb-2013.) |
Ref | Expression |
---|---|
nfmpt.1 | ⊢ Ⅎ𝑥𝐴 |
nfmpt.2 | ⊢ Ⅎ𝑥𝐵 |
Ref | Expression |
---|---|
nfmpt | ⊢ Ⅎ𝑥(𝑦 ∈ 𝐴 ↦ 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-mpt 5006 | . 2 ⊢ (𝑦 ∈ 𝐴 ↦ 𝐵) = {〈𝑦, 𝑧〉 ∣ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐵)} | |
2 | nfmpt.1 | . . . . 5 ⊢ Ⅎ𝑥𝐴 | |
3 | 2 | nfcri 2921 | . . . 4 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐴 |
4 | nfmpt.2 | . . . . 5 ⊢ Ⅎ𝑥𝐵 | |
5 | 4 | nfeq2 2942 | . . . 4 ⊢ Ⅎ𝑥 𝑧 = 𝐵 |
6 | 3, 5 | nfan 1863 | . . 3 ⊢ Ⅎ𝑥(𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐵) |
7 | 6 | nfopab 4994 | . 2 ⊢ Ⅎ𝑥{〈𝑦, 𝑧〉 ∣ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐵)} |
8 | 1, 7 | nfcxfr 2925 | 1 ⊢ Ⅎ𝑥(𝑦 ∈ 𝐴 ↦ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: ∧ wa 387 = wceq 1508 ∈ wcel 2051 Ⅎwnfc 2911 {copab 4988 ↦ cmpt 5005 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1759 ax-4 1773 ax-5 1870 ax-6 1929 ax-7 1966 ax-8 2053 ax-9 2060 ax-10 2080 ax-11 2094 ax-12 2107 ax-13 2302 ax-ext 2745 |
This theorem depends on definitions: df-bi 199 df-an 388 df-or 835 df-tru 1511 df-ex 1744 df-nf 1748 df-sb 2017 df-clab 2754 df-cleq 2766 df-clel 2841 df-nfc 2913 df-opab 4989 df-mpt 5006 |
This theorem is referenced by: ovmpt3rab1 7220 nfof 7231 mpocurryvald 7738 nfrdg 7853 mapxpen 8478 nfoi 8772 seqof2 13242 nfsum1 14906 nfsum 14907 fsumrlim 15025 fsumo1 15026 nfcprod1 15123 nfcprod 15124 gsum2d2 18860 prdsgsum 18864 dprd2d2 18929 gsumdixp 19095 mpfrcl 20024 ptbasfi 21909 ptcnplem 21949 ptcnp 21950 cnmptk2 22014 cnmpt2k 22016 xkocnv 22142 fsumcn 23197 itg2cnlem1 24081 nfitg 24094 itgfsum 24146 dvmptfsum 24291 itgulm2 24716 lgamgulm2 25331 fmptcof2 30182 fpwrelmap 30246 nfesum2 30977 sigapildsys 31099 oms0 31233 bnj1366 31782 nosupbnd2 32770 exrecfnlem 34135 poimirlem26 34392 cdleme32d 37058 cdleme32f 37060 cdlemksv2 37461 cdlemkuv2 37481 hlhilset 38548 aomclem8 39091 binomcxplemdvsum 40137 refsum2cn 40748 fmuldfeq 41325 fprodcnlem 41341 fprodcn 41342 fnlimfv 41405 fnlimcnv 41409 fnlimfvre 41416 fnlimfvre2 41419 fnlimf 41420 fnlimabslt 41421 fprodcncf 41644 dvnmptdivc 41683 dvmptfprod 41690 dvnprodlem1 41691 stoweidlem26 41772 stoweidlem31 41777 stoweidlem34 41780 stoweidlem35 41781 stoweidlem42 41788 stoweidlem48 41794 stoweidlem59 41805 fourierdlem31 41884 fourierdlem112 41964 sge0iunmptlemfi 42156 sge0iunmptlemre 42158 sge0iunmpt 42161 hoicvrrex 42299 ovncvrrp 42307 ovnhoilem1 42344 ovnlecvr2 42353 vonicc 42428 smflim 42514 smfmullem4 42530 smflim2 42541 smflimmpt 42545 smfsup 42549 smfsupmpt 42550 smfinf 42553 smfinfmpt 42554 smflimsuplem2 42556 smflimsuplem5 42559 smflimsup 42563 smflimsupmpt 42564 smfliminf 42566 smfliminfmpt 42567 aacllem 44299 |
Copyright terms: Public domain | W3C validator |