Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > rnex | Structured version Visualization version GIF version |
Description: The range of a set is a set. Corollary 6.8(3) of [TakeutiZaring] p. 26. Similar to Lemma 3D of [Enderton] p. 41. (Contributed by NM, 7-Jul-2008.) |
Ref | Expression |
---|---|
dmex.1 | ⊢ 𝐴 ∈ V |
Ref | Expression |
---|---|
rnex | ⊢ ran 𝐴 ∈ V |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dmex.1 | . 2 ⊢ 𝐴 ∈ V | |
2 | rnexg 7682 | . 2 ⊢ (𝐴 ∈ V → ran 𝐴 ∈ V) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ ran 𝐴 ∈ V |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2110 Vcvv 3408 ran crn 5552 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2016 ax-8 2112 ax-9 2120 ax-ext 2708 ax-sep 5192 ax-nul 5199 ax-pr 5322 ax-un 7523 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 848 df-3an 1091 df-tru 1546 df-fal 1556 df-ex 1788 df-sb 2071 df-clab 2715 df-cleq 2729 df-clel 2816 df-rab 3070 df-v 3410 df-dif 3869 df-un 3871 df-in 3873 df-ss 3883 df-nul 4238 df-if 4440 df-sn 4542 df-pr 4544 df-op 4548 df-uni 4820 df-br 5054 df-opab 5116 df-cnv 5559 df-dm 5561 df-rn 5562 |
This theorem is referenced by: elxp4 7700 elxp5 7701 ffoss 7719 fvclex 7732 wemoiso2 7747 2ndval 7764 fo2nd 7782 mapfoss 8533 ixpsnf1o 8619 bren 8636 brenOLD 8637 sucdom2 8755 mapen 8810 ssenen 8820 fodomfib 8950 hartogslem1 9158 brwdom 9183 unxpwdom2 9204 noinfep 9275 trpredex 9343 r0weon 9626 fseqen 9641 acnlem 9662 infpwfien 9676 aceq3lem 9734 dfac4 9736 dfac5 9742 dfac2b 9744 dfac9 9750 dfac12lem2 9758 dfac12lem3 9759 infmap2 9832 cfflb 9873 infpssr 9922 fin23lem14 9947 fin23lem16 9949 fin23lem17 9952 fin23lem38 9963 fin23lem39 9964 axdc2lem 10062 axdc3lem2 10065 axcclem 10071 ttukeylem6 10128 wunex2 10352 wuncval2 10361 intgru 10428 wfgru 10430 qexALT 12560 seqexw 13590 hashfacenOLD 14019 shftfval 14633 vdwapval 16526 restfn 16929 prdsvallem 16959 prdsval 16960 wunfunc 17405 wunfuncOLD 17406 wunnat 17463 wunnatOLD 17464 arwval 17549 catcfuccl 17625 catcfucclOLD 17626 catcxpccl 17714 catcxpcclOLD 17715 yon11 17772 yon12 17773 yon2 17774 yonpropd 17776 oppcyon 17777 yonffth 17792 yoniso 17793 plusffval 18120 grpsubfval 18411 mulgfval 18490 sylow1lem2 18988 sylow2blem1 19009 sylow2blem2 19010 sylow3lem1 19016 sylow3lem6 19021 dmdprd 19385 dprdval 19390 staffval 19883 scaffval 19917 lpival 20283 ipffval 20610 cmpsub 22297 2ndcsep 22356 1stckgen 22451 kgencn2 22454 txcmplem1 22538 blbas 23328 met1stc 23419 psmetutop 23465 nmfval 23486 dchrptlem2 26146 dchrptlem3 26147 ishpg 26850 edgval 27140 bafval 28685 vsfval 28714 foresf1o 30569 fnpreimac 30728 nsgmgc 31311 nsgqusf1o 31315 idlsrgtset 31367 locfinreflem 31504 cmpcref 31514 rspectopn 31531 ordtconnlem1 31588 qqhval 31636 sigapildsys 31842 dya2icoseg2 31957 dya2iocuni 31962 sxbrsigalem2 31965 sxbrsigalem5 31967 omssubadd 31979 mvtval 33175 mvrsval 33180 mstaval 33219 brrestrict 33988 relowlssretop 35271 exrecfnlem 35287 ctbssinf 35314 lindsdom 35508 indexdom 35629 heiborlem1 35706 isdrngo2 35853 isrngohom 35860 idlval 35908 isidl 35909 igenval 35956 lsatset 36741 dicval 38927 trclexi 40904 rtrclexi 40905 dfrtrcl5 40913 dfrcl2 40959 stoweidlem59 43275 fourierdlem71 43393 salgensscntex 43558 aacllem 46176 |
Copyright terms: Public domain | W3C validator |