![]() |
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 6866 | . 2 ⊢ (℩𝑥 ∈ 𝐴 𝜓) = (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜓)) | |
2 | iotaex 6103 | . 2 ⊢ (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜓)) ∈ V | |
3 | 1, 2 | eqeltri 2902 | 1 ⊢ (℩𝑥 ∈ 𝐴 𝜓) ∈ V |
Colors of variables: wff setvar class |
Syntax hints: ∧ wa 386 ∈ wcel 2164 Vcvv 3414 ℩cio 6084 ℩crio 6865 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1894 ax-4 1908 ax-5 2009 ax-6 2075 ax-7 2112 ax-9 2173 ax-10 2192 ax-11 2207 ax-12 2220 ax-13 2389 ax-ext 2803 ax-nul 5013 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 879 df-tru 1660 df-ex 1879 df-nf 1883 df-sb 2068 df-mo 2605 df-eu 2640 df-clab 2812 df-cleq 2818 df-clel 2821 df-nfc 2958 df-ral 3122 df-rex 3123 df-v 3416 df-sbc 3663 df-dif 3801 df-un 3803 df-in 3805 df-ss 3812 df-nul 4145 df-sn 4398 df-pr 4400 df-uni 4659 df-iota 6086 df-riota 6866 |
This theorem is referenced by: ordtypelem3 8694 dfac8clem 9168 zorn2lem1 9633 subval 10592 1div0 11011 divval 11012 elq 12073 flval 12890 ceilval2 12936 cjval 14219 sqrtval 14354 sqrtf 14480 cidval 16690 cidfn 16692 lubdm 17332 lubval 17337 glbdm 17345 glbval 17350 grpinvval 17815 grpinvfn 17816 pj1val 18459 evlsval 19879 q1pval 24312 ig1pval 24331 coeval 24378 quotval 24446 mirfv 25968 mirf 25972 usgredg2v 26523 frgrncvvdeqlem5 27673 1div0apr 27871 gidval 27911 grpoinvval 27922 grpoinvf 27931 pjhval 28800 pjfni 29104 cnlnadjlem5 29474 nmopadjlei 29491 cdj3lem2 29838 xdivval 30161 cvmlift3lem4 31839 scutval 32439 dmscut 32446 fvtransport 32667 finxpreclem4 33769 poimirlem26 33972 lshpkrlem1 35178 lshpkrlem2 35179 lshpkrlem3 35180 trlval 36230 cdleme31fv 36458 cdleme50f 36610 cdlemksv 36912 cdlemkuu 36963 cdlemk40 36985 cdlemk56 37039 cdlemm10N 37186 cdlemn11a 37275 dihval 37300 dihf11lem 37334 dihatlat 37402 dochfl1 37544 mapdhval 37792 hvmapvalvalN 37829 hdmap1vallem 37865 hdmapval 37896 hdmapfnN 37897 hgmapval 37955 hgmapfnN 37956 resubval 38064 mpaaval 38557 wessf1ornlem 40172 |
Copyright terms: Public domain | W3C validator |