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 7121 | . 2 ⊢ (℩𝑥 ∈ 𝐴 𝜓) = (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜓)) | |
2 | iotaex 6313 | . 2 ⊢ (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜓)) ∈ V | |
3 | 1, 2 | eqeltri 2829 | 1 ⊢ (℩𝑥 ∈ 𝐴 𝜓) ∈ V |
Colors of variables: wff setvar class |
Syntax hints: ∧ wa 399 ∈ wcel 2113 Vcvv 3397 ℩cio 6289 ℩crio 7120 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1916 ax-6 1974 ax-7 2019 ax-8 2115 ax-9 2123 ax-10 2144 ax-11 2161 ax-12 2178 ax-ext 2710 ax-nul 5171 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 847 df-tru 1545 df-fal 1555 df-ex 1787 df-nf 1791 df-sb 2074 df-mo 2540 df-eu 2570 df-clab 2717 df-cleq 2730 df-clel 2811 df-ral 3058 df-rex 3059 df-v 3399 df-sbc 3680 df-dif 3844 df-un 3846 df-in 3848 df-ss 3858 df-nul 4210 df-sn 4514 df-pr 4516 df-uni 4794 df-iota 6291 df-riota 7121 |
This theorem is referenced by: ordtypelem3 9050 dfac8clem 9525 zorn2lem1 9989 subval 10948 1div0 11370 divval 11371 elq 12425 flval 13248 ceilval2 13294 cjval 14544 sqrtval 14679 sqrtf 14806 cidval 17044 cidfn 17046 lubdm 17698 lubval 17703 glbdm 17711 glbval 17716 grpinvfval 18253 grpinvval 18255 grpinvfn 18256 pj1val 18932 evlsval 20893 q1pval 24898 ig1pval 24917 coeval 24964 quotval 25032 mirfv 26594 mirf 26598 usgredg2v 27161 frgrncvvdeqlem5 28232 1div0apr 28397 gidval 28439 grpoinvval 28450 grpoinvf 28459 pjhval 29324 pjfni 29628 cnlnadjlem5 29998 nmopadjlei 30015 cdj3lem2 30362 xdivval 30760 cvmlift3lem4 32847 scutval 33627 dmscut 33638 fvtransport 33964 finxpreclem4 35177 poimirlem26 35415 lshpkrlem1 36736 lshpkrlem2 36737 lshpkrlem3 36738 trlval 37788 cdleme31fv 38016 cdleme50f 38168 cdlemksv 38470 cdlemkuu 38521 cdlemk40 38543 cdlemk56 38597 cdlemm10N 38744 cdlemn11a 38833 dihval 38858 dihf11lem 38892 dihatlat 38960 dochfl1 39102 mapdhval 39350 hvmapvalvalN 39387 hdmap1vallem 39423 hdmapval 39454 hdmapfnN 39455 hgmapval 39513 hgmapfnN 39514 resubval 39911 mpaaval 40532 wessf1ornlem 42244 |
Copyright terms: Public domain | W3C validator |