Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > elrnmpti | Structured version Visualization version GIF 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 | ⊢ 𝐵 ∈ V |
Ref | Expression |
---|---|
elrnmpti | ⊢ (𝐶 ∈ ran 𝐹 ↔ ∃𝑥 ∈ 𝐴 𝐶 = 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elrnmpti.2 | . . 3 ⊢ 𝐵 ∈ V | |
2 | 1 | rgenw 3074 | . 2 ⊢ ∀𝑥 ∈ 𝐴 𝐵 ∈ V |
3 | rnmpt.1 | . . 3 ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) | |
4 | 3 | elrnmptg 5843 | . 2 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ V → (𝐶 ∈ ran 𝐹 ↔ ∃𝑥 ∈ 𝐴 𝐶 = 𝐵)) |
5 | 2, 4 | ax-mp 5 | 1 ⊢ (𝐶 ∈ ran 𝐹 ↔ ∃𝑥 ∈ 𝐴 𝐶 = 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 209 = wceq 1543 ∈ wcel 2111 ∀wral 3062 ∃wrex 3063 Vcvv 3421 ↦ cmpt 5150 ran crn 5567 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2016 ax-8 2113 ax-9 2121 ax-10 2142 ax-11 2159 ax-12 2176 ax-ext 2709 ax-sep 5207 ax-nul 5214 ax-pr 5337 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 848 df-3an 1091 df-tru 1546 df-fal 1556 df-ex 1788 df-nf 1792 df-sb 2072 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2817 df-nfc 2887 df-ral 3067 df-rex 3068 df-rab 3071 df-v 3423 df-dif 3884 df-un 3886 df-in 3888 df-ss 3898 df-nul 4253 df-if 4455 df-sn 4557 df-pr 4559 df-op 4563 df-br 5069 df-opab 5131 df-mpt 5151 df-cnv 5574 df-dm 5576 df-rn 5577 |
This theorem is referenced by: fliftel 7137 oarec 8311 unfilem1 8960 pwfilemOLD 8995 elrest 16957 psgneldm2 18921 psgnfitr 18934 iscyggen2 19290 iscyg3 19295 cycsubgcyg 19311 eldprd 19416 leordtval2 22133 iocpnfordt 22136 icomnfordt 22137 lecldbas 22140 tsmsxplem1 23074 minveclem2 24347 lhop2 24936 taylthlem2 25290 fsumvma 26118 dchrptlem2 26170 2sqlem1 26322 dchrisum0fno1 26416 minvecolem2 28980 swrdrn3 30971 nsgqusf1olem1 31336 nsgqusf1olem3 31338 rspectopn 31555 zarclsun 31558 zarcls 31562 gsumesum 31763 esumlub 31764 esumcst 31767 esumpcvgval 31782 esumgect 31794 esum2d 31797 sigapildsys 31866 sxbrsigalem2 31989 omssubaddlem 32002 omssubadd 32003 eulerpartgbij 32075 actfunsnf1o 32320 actfunsnrndisj 32321 reprsuc 32331 breprexplema 32346 bnj1366 32545 msubco 33229 msubvrs 33258 fin2so 35528 poimirlem17 35558 poimirlem20 35561 cntotbnd 35718 islsat 36769 |
Copyright terms: Public domain | W3C validator |