![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > elrnmpti | Structured version Visualization version Unicode version |
Description: Membership in the range of a function. (Contributed by NM, 30-Aug-2004.) (Revised by Mario Carneiro, 31-Aug-2015.) |
Ref | Expression |
---|---|
rnmpt.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
elrnmpti.2 |
![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
elrnmpti |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elrnmpti.2 |
. . 3
![]() ![]() ![]() ![]() | |
2 | 1 | rgenw 2748 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | rnmpt.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 3 | elrnmptg 5083 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | 2, 4 | ax-mp 5 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1668 ax-4 1681 ax-5 1757 ax-6 1804 ax-7 1850 ax-9 1895 ax-10 1914 ax-11 1919 ax-12 1932 ax-13 2090 ax-ext 2430 ax-sep 4524 ax-nul 4533 ax-pr 4638 |
This theorem depends on definitions: df-bi 189 df-or 372 df-an 373 df-3an 986 df-tru 1446 df-ex 1663 df-nf 1667 df-sb 1797 df-eu 2302 df-mo 2303 df-clab 2437 df-cleq 2443 df-clel 2446 df-nfc 2580 df-ne 2623 df-ral 2741 df-rex 2742 df-rab 2745 df-v 3046 df-dif 3406 df-un 3408 df-in 3410 df-ss 3417 df-nul 3731 df-if 3881 df-sn 3968 df-pr 3970 df-op 3974 df-br 4402 df-opab 4461 df-mpt 4462 df-cnv 4841 df-dm 4843 df-rn 4844 |
This theorem is referenced by: fliftel 6200 oarec 7260 unfilem1 7832 pwfilem 7865 elrest 15319 psgneldm2 17138 psgnfitr 17151 iscyggen2 17509 iscyg3 17514 cycsubgcyg 17528 eldprd 17629 leordtval2 20221 iocpnfordt 20224 icomnfordt 20225 lecldbas 20228 tsmsxplem1 21160 minveclem2 22361 minveclem2OLD 22373 lhop2 22960 taylthlem2 23322 fsumvma 24134 dchrptlem2 24186 2sqlem1 24284 dchrisum0fno1 24342 minvecolem2 26510 minvecolem2OLD 26520 gsumesum 28873 esumlub 28874 esumcst 28877 esumpcvgval 28892 esumgect 28904 esum2d 28907 sigapildsys 28977 sxbrsigalem2 29101 omssubaddlem 29120 omssubadd 29121 omssubaddlemOLD 29124 omssubaddOLD 29125 eulerpartgbij 29198 bnj1366 29634 msubco 30162 msubvrs 30191 fin2so 31925 poimirlem17 31950 poimirlem20 31953 cntotbnd 32121 islsat 32551 |
Copyright terms: Public domain | W3C validator |