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 4645 | . 2 ⊢ (𝑦 ∈ 𝐴 ↦ 𝐵) = {〈𝑦, 𝑧〉 ∣ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐵)} | |
2 | nfmpt.1 | . . . . 5 ⊢ Ⅎ𝑥𝐴 | |
3 | 2 | nfcri 2745 | . . . 4 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐴 |
4 | nfmpt.2 | . . . . 5 ⊢ Ⅎ𝑥𝐵 | |
5 | 4 | nfeq2 2766 | . . . 4 ⊢ Ⅎ𝑥 𝑧 = 𝐵 |
6 | 3, 5 | nfan 1816 | . . 3 ⊢ Ⅎ𝑥(𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐵) |
7 | 6 | nfopab 4650 | . 2 ⊢ Ⅎ𝑥{〈𝑦, 𝑧〉 ∣ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐵)} |
8 | 1, 7 | nfcxfr 2749 | 1 ⊢ Ⅎ𝑥(𝑦 ∈ 𝐴 ↦ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: ∧ wa 383 = wceq 1475 ∈ wcel 1977 Ⅎwnfc 2738 {copab 4642 ↦ cmpt 4643 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-opab 4644 df-mpt 4645 |
This theorem is referenced by: ovmpt3rab1 6789 mpt2curryvald 7283 nfrdg 7397 mapxpen 8011 nfoi 8302 seqof2 12721 nfsum1 14268 nfsum 14269 fsumrlim 14384 fsumo1 14385 nfcprod1 14479 nfcprod 14480 gsum2d2 18196 prdsgsum 18200 dprd2d2 18266 gsumdixp 18432 mpfrcl 19339 ptbasfi 21194 ptcnplem 21234 ptcnp 21235 cnmptk2 21299 cnmpt2k 21301 xkocnv 21427 fsumcn 22481 itg2cnlem1 23334 nfitg 23347 itgfsum 23399 dvmptfsum 23542 itgulm2 23967 lgamgulm2 24562 fmptcof2 28839 fpwrelmap 28896 nfesum2 29430 sigapildsys 29552 oms0 29686 bnj1366 30154 poimirlem26 32605 cdleme32d 34750 cdleme32f 34752 cdlemksv2 35153 cdlemkuv2 35173 hlhilset 36244 aomclem8 36649 binomcxplemdvsum 37576 refsum2cn 38220 wessf1ornlem 38366 fmuldfeq 38650 fprodcnlem 38666 fprodcn 38667 fnlimfv 38730 fnlimcnv 38734 fnlimfvre 38741 fnlimfvre2 38744 fnlimf 38745 fnlimabslt 38746 fprodcncf 38787 dvnmptdivc 38828 dvmptfprod 38835 dvnprodlem1 38836 stoweidlem26 38919 stoweidlem31 38924 stoweidlem34 38927 stoweidlem35 38928 stoweidlem42 38935 stoweidlem48 38941 stoweidlem59 38952 fourierdlem31 39031 fourierdlem112 39111 sge0iunmptlemfi 39306 sge0iunmptlemre 39308 sge0iunmpt 39311 hoicvrrex 39446 ovncvrrp 39454 ovnhoilem1 39491 ovnlecvr2 39500 vonicc 39576 smflim 39663 smfmullem4 39679 aacllem 42356 |
Copyright terms: Public domain | W3C validator |