![]() |
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 7382 | . 2 ⊢ (℩𝑥 ∈ 𝐴 𝜓) = (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜓)) | |
2 | iotaex 6526 | . 2 ⊢ (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜓)) ∈ V | |
3 | 1, 2 | eqeltri 2825 | 1 ⊢ (℩𝑥 ∈ 𝐴 𝜓) ∈ V |
Colors of variables: wff setvar class |
Syntax hints: ∧ wa 394 ∈ wcel 2098 Vcvv 3473 ℩cio 6503 ℩crio 7381 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-ext 2699 ax-nul 5310 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-tru 1536 df-fal 1546 df-ex 1774 df-sb 2060 df-clab 2706 df-cleq 2720 df-clel 2806 df-ne 2938 df-v 3475 df-dif 3952 df-un 3954 df-in 3956 df-ss 3966 df-nul 4327 df-sn 4633 df-pr 4635 df-uni 4913 df-iota 6505 df-riota 7382 |
This theorem is referenced by: ordtypelem3 9551 dfac8clem 10063 zorn2lem1 10527 subval 11489 1div0 11911 divval 11912 elq 12972 flval 13799 ceilval2 13845 cjval 15089 sqrtval 15224 sqrtf 15350 cidval 17664 cidfn 17666 lubdm 18350 lubval 18355 glbdm 18363 glbval 18368 grpinvfval 18942 grpinvval 18944 grpinvfn 18945 pj1val 19657 evlsval 22039 q1pval 26110 ig1pval 26130 coeval 26177 quotval 26247 scutval 27753 dmscut 27764 divsval 28109 mirfv 28480 mirf 28484 usgredg2v 29060 frgrncvvdeqlem5 30133 1div0apr 30298 gidval 30342 grpoinvval 30353 grpoinvf 30362 pjhval 31227 pjfni 31531 cnlnadjlem5 31901 nmopadjlei 31918 cdj3lem2 32265 xdivval 32663 cvmlift3lem4 34965 fvtransport 35661 finxpreclem4 36906 poimirlem26 37152 lshpkrlem1 38614 lshpkrlem2 38615 lshpkrlem3 38616 trlval 39667 cdleme31fv 39895 cdleme50f 40047 cdlemksv 40349 cdlemkuu 40400 cdlemk40 40422 cdlemk56 40476 cdlemm10N 40623 cdlemn11a 40712 dihval 40737 dihf11lem 40771 dihatlat 40839 dochfl1 40981 mapdhval 41229 hvmapvalvalN 41266 hdmap1vallem 41302 hdmapval 41333 hdmapfnN 41334 hgmapval 41392 hgmapfnN 41393 resubval 41953 mpaaval 42606 wessf1ornlem 44588 |
Copyright terms: Public domain | W3C validator |