Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > imaex | Structured version Visualization version GIF version |
Description: The image of a set is a set. Theorem 3.17 of [Monk1] p. 39. (Contributed by JJ, 24-Sep-2021.) |
Ref | Expression |
---|---|
imaex.1 | ⊢ 𝐴 ∈ V |
Ref | Expression |
---|---|
imaex | ⊢ (𝐴 “ 𝐵) ∈ V |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | imaex.1 | . 2 ⊢ 𝐴 ∈ V | |
2 | imaexg 7622 | . 2 ⊢ (𝐴 ∈ V → (𝐴 “ 𝐵) ∈ V) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (𝐴 “ 𝐵) ∈ V |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2114 Vcvv 3496 “ cima 5560 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2161 ax-12 2177 ax-ext 2795 ax-sep 5205 ax-nul 5212 ax-pr 5332 ax-un 7463 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3an 1085 df-tru 1540 df-ex 1781 df-nf 1785 df-sb 2070 df-mo 2622 df-eu 2654 df-clab 2802 df-cleq 2816 df-clel 2895 df-nfc 2965 df-ral 3145 df-rex 3146 df-rab 3149 df-v 3498 df-dif 3941 df-un 3943 df-in 3945 df-ss 3954 df-nul 4294 df-if 4470 df-sn 4570 df-pr 4572 df-op 4576 df-uni 4841 df-br 5069 df-opab 5131 df-xp 5563 df-cnv 5565 df-dm 5567 df-rn 5568 df-res 5569 df-ima 5570 |
This theorem is referenced by: frxp 7822 pw2f1o 8624 ssenen 8693 fiint 8797 fissuni 8831 fipreima 8832 marypha1lem 8899 infxpenlem 9441 ackbij2lem2 9664 enfin2i 9745 fin1a2lem7 9830 fpwwe 10070 canthwelem 10074 tskuni 10207 isacs4lem 17780 gicsubgen 18420 gsumzaddlem 19043 isunit 19409 evpmss 20732 psgnevpmb 20733 ptbasfi 22191 hmphdis 22406 ustuqtop0 22851 utopsnneiplem 22858 neipcfilu 22907 nghmfval 23333 qtopbaslem 23369 fta1glem2 24762 fta1blem 24764 lgsqrlem4 25927 legval 26372 evpmval 30789 altgnsg 30793 brapply 33401 dfrdg4 33414 ptrest 34893 intima0 39999 elintima 40005 brtrclfv2 40079 |
Copyright terms: Public domain | W3C validator |