![]() |
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 6753 | . 2 ⊢ (℩𝑥 ∈ 𝐴 𝜓) = (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜓)) | |
2 | iotaex 6011 | . 2 ⊢ (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜓)) ∈ V | |
3 | 1, 2 | eqeltri 2845 | 1 ⊢ (℩𝑥 ∈ 𝐴 𝜓) ∈ V |
Colors of variables: wff setvar class |
Syntax hints: ∧ wa 382 ∈ wcel 2144 Vcvv 3349 ℩cio 5992 ℩crio 6752 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1869 ax-4 1884 ax-5 1990 ax-6 2056 ax-7 2092 ax-9 2153 ax-10 2173 ax-11 2189 ax-12 2202 ax-13 2407 ax-ext 2750 ax-nul 4920 |
This theorem depends on definitions: df-bi 197 df-an 383 df-or 827 df-tru 1633 df-ex 1852 df-nf 1857 df-sb 2049 df-eu 2621 df-clab 2757 df-cleq 2763 df-clel 2766 df-nfc 2901 df-ral 3065 df-rex 3066 df-v 3351 df-sbc 3586 df-dif 3724 df-un 3726 df-in 3728 df-ss 3735 df-nul 4062 df-sn 4315 df-pr 4317 df-uni 4573 df-iota 5994 df-riota 6753 |
This theorem is referenced by: ordtypelem3 8580 dfac8clem 9054 zorn2lem1 9519 subval 10473 1div0 10887 divval 10888 elq 11992 flval 12802 ceilval2 12848 cjval 14049 sqrtval 14184 sqrtf 14310 cidval 16544 cidfn 16546 lubdm 17186 lubval 17191 glbdm 17199 glbval 17204 grpinvval 17668 grpinvfn 17669 pj1val 18314 evlsval 19733 q1pval 24132 ig1pval 24151 coeval 24198 quotval 24266 mirfv 25771 mirf 25775 usgredg2v 26340 frgrncvvdeqlem5 27482 1div0apr 27660 gidval 27700 grpoinvval 27711 grpoinvf 27720 pjhval 28590 pjfni 28894 cnlnadjlem5 29264 nmopadjlei 29281 cdj3lem2 29628 xdivval 29961 cvmlift3lem4 31636 scutval 32242 dmscut 32249 fvtransport 32470 finxpreclem4 33561 poimirlem26 33761 lshpkrlem1 34912 lshpkrlem2 34913 lshpkrlem3 34914 trlval 35964 cdleme31fv 36192 cdleme50f 36344 cdlemksv 36646 cdlemkuu 36697 cdlemk40 36719 cdlemk56 36773 cdlemm10N 36921 cdlemn11a 37010 dihval 37035 dihf11lem 37069 dihatlat 37137 dochfl1 37279 mapdhval 37527 hvmapvalvalN 37564 hdmap1vallem 37600 hdmapval 37631 hdmapfnN 37632 hgmapval 37690 hgmapfnN 37691 mpaaval 38240 wessf1ornlem 39885 |
Copyright terms: Public domain | W3C validator |