![]() |
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 5233 | . 2 ⊢ (𝑦 ∈ 𝐴 ↦ 𝐵) = {〈𝑦, 𝑧〉 ∣ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐵)} | |
2 | nfmpt.1 | . . . . 5 ⊢ Ⅎ𝑥𝐴 | |
3 | 2 | nfcri 2882 | . . . 4 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐴 |
4 | nfmpt.2 | . . . . 5 ⊢ Ⅎ𝑥𝐵 | |
5 | 4 | nfeq2 2909 | . . . 4 ⊢ Ⅎ𝑥 𝑧 = 𝐵 |
6 | 3, 5 | nfan 1894 | . . 3 ⊢ Ⅎ𝑥(𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐵) |
7 | 6 | nfopab 5218 | . 2 ⊢ Ⅎ𝑥{〈𝑦, 𝑧〉 ∣ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐵)} |
8 | 1, 7 | nfcxfr 2889 | 1 ⊢ Ⅎ𝑥(𝑦 ∈ 𝐴 ↦ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: ∧ wa 394 = wceq 1533 ∈ wcel 2098 Ⅎwnfc 2875 {copab 5211 ↦ cmpt 5232 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-10 2129 ax-11 2146 ax-12 2166 ax-ext 2696 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-tru 1536 df-ex 1774 df-nf 1778 df-sb 2060 df-clab 2703 df-cleq 2717 df-clel 2802 df-nfc 2877 df-opab 5212 df-mpt 5233 |
This theorem is referenced by: ovmpt3rab1 7679 nfof 7691 mpocurryvald 8276 nfrdg 8435 mapxpen 9168 nfoi 9539 seqof2 14061 nfsum1 15672 nfsum 15673 fsumrlim 15793 fsumo1 15794 nfcprod1 15890 nfcprod 15891 gsum2d2 19941 prdsgsum 19948 dprd2d2 20013 gsumdixp 20267 mpfrcl 22053 ptbasfi 23529 ptcnplem 23569 ptcnp 23570 cnmptk2 23634 cnmpt2k 23636 xkocnv 23762 fsumcn 24832 itg2cnlem1 25735 nfitg 25748 itgfsum 25800 dvmptfsum 25951 itgulm2 26390 lgamgulm2 27013 nosupbnd2 27695 noinfbnd2 27710 fmptcof2 32524 fpwrelmap 32597 nfesum2 33788 sigapildsys 33909 oms0 34045 bnj1366 34588 exrecfnlem 36986 poimirlem26 37247 cdleme32d 40044 cdleme32f 40046 cdlemksv2 40447 cdlemkuv2 40467 hlhilset 41534 pwsgprod 41909 aomclem8 42624 binomcxplemdvsum 43931 refsum2cn 44539 fmuldfeq 45106 fprodcnlem 45122 fprodcn 45123 fnlimfv 45186 fnlimcnv 45190 fnlimfvre 45197 fnlimfvre2 45200 fnlimf 45201 fnlimabslt 45202 fprodcncf 45423 dvnmptdivc 45461 dvmptfprod 45468 dvnprodlem1 45469 stoweidlem26 45549 stoweidlem31 45554 stoweidlem34 45557 stoweidlem35 45558 stoweidlem42 45565 stoweidlem48 45571 stoweidlem59 45582 fourierdlem31 45661 fourierdlem112 45741 sge0iunmptlemfi 45936 sge0iunmptlemre 45938 sge0iunmpt 45941 hoicvrrex 46079 ovncvrrp 46087 ovnhoilem1 46124 ovnlecvr2 46133 vonicc 46208 smflim 46300 smfmullem4 46317 smflim2 46329 smflimmpt 46333 smfsup 46337 smfsupmpt 46338 smfinf 46341 smfinfmpt 46342 smflimsuplem2 46344 smflimsuplem5 46347 smflimsup 46351 smflimsupmpt 46352 smfliminf 46354 smfliminfmpt 46355 fsupdm 46365 finfdm 46369 aacllem 48417 |
Copyright terms: Public domain | W3C validator |