Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > riotaex | Structured version Visualization version GIF version |
Description: Restricted iota is a set. (Contributed by NM, 15-Sep-2011.) |
Ref | Expression |
---|---|
riotaex | ⊢ (℩𝑥 ∈ 𝐴 𝜓) ∈ V |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-riota 7232 | . 2 ⊢ (℩𝑥 ∈ 𝐴 𝜓) = (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜓)) | |
2 | iotaex 6413 | . 2 ⊢ (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜓)) ∈ V | |
3 | 1, 2 | eqeltri 2835 | 1 ⊢ (℩𝑥 ∈ 𝐴 𝜓) ∈ V |
Colors of variables: wff setvar class |
Syntax hints: ∧ wa 396 ∈ wcel 2106 Vcvv 3432 ℩cio 6389 ℩crio 7231 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2709 ax-nul 5230 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-tru 1542 df-fal 1552 df-ex 1783 df-nf 1787 df-sb 2068 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2816 df-ral 3069 df-rex 3070 df-v 3434 df-dif 3890 df-un 3892 df-in 3894 df-ss 3904 df-nul 4257 df-sn 4562 df-pr 4564 df-uni 4840 df-iota 6391 df-riota 7232 |
This theorem is referenced by: ordtypelem3 9279 dfac8clem 9788 zorn2lem1 10252 subval 11212 1div0 11634 divval 11635 elq 12690 flval 13514 ceilval2 13560 cjval 14813 sqrtval 14948 sqrtf 15075 cidval 17386 cidfn 17388 lubdm 18069 lubval 18074 glbdm 18082 glbval 18087 grpinvfval 18618 grpinvval 18620 grpinvfn 18621 pj1val 19301 evlsval 21296 q1pval 25318 ig1pval 25337 coeval 25384 quotval 25452 mirfv 27017 mirf 27021 usgredg2v 27594 frgrncvvdeqlem5 28667 1div0apr 28832 gidval 28874 grpoinvval 28885 grpoinvf 28894 pjhval 29759 pjfni 30063 cnlnadjlem5 30433 nmopadjlei 30450 cdj3lem2 30797 xdivval 31193 cvmlift3lem4 33284 scutval 33994 dmscut 34005 fvtransport 34334 finxpreclem4 35565 poimirlem26 35803 lshpkrlem1 37124 lshpkrlem2 37125 lshpkrlem3 37126 trlval 38176 cdleme31fv 38404 cdleme50f 38556 cdlemksv 38858 cdlemkuu 38909 cdlemk40 38931 cdlemk56 38985 cdlemm10N 39132 cdlemn11a 39221 dihval 39246 dihf11lem 39280 dihatlat 39348 dochfl1 39490 mapdhval 39738 hvmapvalvalN 39775 hdmap1vallem 39811 hdmapval 39842 hdmapfnN 39843 hgmapval 39901 hgmapfnN 39902 resubval 40350 mpaaval 40976 wessf1ornlem 42722 |
Copyright terms: Public domain | W3C validator |