| 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 5226 | . 2 ⊢ (𝑦 ∈ 𝐴 ↦ 𝐵) = {〈𝑦, 𝑧〉 ∣ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐵)} | |
| 2 | nfmpt.1 | . . . . 5 ⊢ Ⅎ𝑥𝐴 | |
| 3 | 2 | nfcri 2897 | . . . 4 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐴 |
| 4 | nfmpt.2 | . . . . 5 ⊢ Ⅎ𝑥𝐵 | |
| 5 | 4 | nfeq2 2923 | . . . 4 ⊢ Ⅎ𝑥 𝑧 = 𝐵 |
| 6 | 3, 5 | nfan 1899 | . . 3 ⊢ Ⅎ𝑥(𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐵) |
| 7 | 6 | nfopab 5212 | . 2 ⊢ Ⅎ𝑥{〈𝑦, 𝑧〉 ∣ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐵)} |
| 8 | 1, 7 | nfcxfr 2903 | 1 ⊢ Ⅎ𝑥(𝑦 ∈ 𝐴 ↦ 𝐵) |
| Colors of variables: wff setvar class |
| Syntax hints: ∧ wa 395 = wceq 1540 ∈ wcel 2108 Ⅎwnfc 2890 {copab 5205 ↦ cmpt 5225 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2157 ax-12 2177 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-tru 1543 df-ex 1780 df-nf 1784 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-nfc 2892 df-opab 5206 df-mpt 5226 |
| This theorem is referenced by: ovmpt3rab1 7691 nfof 7703 mpocurryvald 8295 nfrdg 8454 mapxpen 9183 nfoi 9554 seqof2 14101 nfsum1 15726 nfsum 15727 fsumrlim 15847 fsumo1 15848 nfcprod1 15944 nfcprod 15945 gsum2d2 19992 prdsgsum 19999 dprd2d2 20064 gsumdixp 20316 mpfrcl 22109 ptbasfi 23589 ptcnplem 23629 ptcnp 23630 cnmptk2 23694 cnmpt2k 23696 xkocnv 23822 fsumcn 24894 itg2cnlem1 25796 nfitg 25810 itgfsum 25862 dvmptfsum 26013 itgulm2 26452 lgamgulm2 27079 nosupbnd2 27761 noinfbnd2 27776 fmptcof2 32667 fpwrelmap 32744 nfesum2 34042 sigapildsys 34163 oms0 34299 bnj1366 34843 exrecfnlem 37380 poimirlem26 37653 cdleme32d 40446 cdleme32f 40448 cdlemksv2 40849 cdlemkuv2 40869 hlhilset 41936 pwsgprod 42554 aomclem8 43073 binomcxplemdvsum 44374 refsum2cn 45043 fmuldfeq 45598 fprodcnlem 45614 fprodcn 45615 fnlimfv 45678 fnlimcnv 45682 fnlimfvre 45689 fnlimfvre2 45692 fnlimf 45693 fnlimabslt 45694 fprodcncf 45915 dvnmptdivc 45953 dvmptfprod 45960 dvnprodlem1 45961 stoweidlem26 46041 stoweidlem31 46046 stoweidlem34 46049 stoweidlem35 46050 stoweidlem42 46057 stoweidlem48 46063 stoweidlem59 46074 fourierdlem31 46153 fourierdlem112 46233 sge0iunmptlemfi 46428 sge0iunmptlemre 46430 sge0iunmpt 46433 hoicvrrex 46571 ovncvrrp 46579 ovnhoilem1 46616 ovnlecvr2 46625 vonicc 46700 smflim 46792 smfmullem4 46809 smflim2 46821 smflimmpt 46825 smfsup 46829 smfsupmpt 46830 smfinf 46833 smfinfmpt 46834 smflimsuplem2 46836 smflimsuplem5 46839 smflimsup 46843 smflimsupmpt 46844 smfliminf 46846 smfliminfmpt 46847 fsupdm 46857 finfdm 46861 aacllem 49320 |
| Copyright terms: Public domain | W3C validator |