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 7639 | . 2 ⊢ (𝐴 ∈ V → (𝐴 “ 𝐵) ∈ V) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (𝐴 “ 𝐵) ∈ V |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2113 Vcvv 3397 “ cima 5522 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1916 ax-6 1974 ax-7 2019 ax-8 2115 ax-9 2123 ax-ext 2710 ax-sep 5164 ax-nul 5171 ax-pr 5293 ax-un 7473 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 847 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1787 df-sb 2074 df-clab 2717 df-cleq 2730 df-clel 2811 df-ral 3058 df-rex 3059 df-rab 3062 df-v 3399 df-dif 3844 df-un 3846 df-in 3848 df-ss 3858 df-nul 4210 df-if 4412 df-sn 4514 df-pr 4516 df-op 4520 df-uni 4794 df-br 5028 df-opab 5090 df-xp 5525 df-cnv 5527 df-dm 5529 df-rn 5530 df-res 5531 df-ima 5532 |
This theorem is referenced by: frxp 7839 pw2f1o 8664 ssenen 8734 fiint 8862 fissuni 8895 fipreima 8896 marypha1lem 8963 infxpenlem 9506 ackbij2lem2 9733 enfin2i 9814 fin1a2lem7 9899 fpwwe 10139 canthwelem 10143 tskuni 10276 isacs4lem 17887 gicsubgen 18529 gsumzaddlem 19153 isunit 19522 evpmss 20395 psgnevpmb 20396 ptbasfi 22325 hmphdis 22540 ustuqtop0 22985 utopsnneiplem 22992 neipcfilu 23041 nghmfval 23468 qtopbaslem 23504 fta1glem2 24911 fta1blem 24913 lgsqrlem4 26077 legval 26522 evpmval 30981 altgnsg 30985 elrspunidl 31170 zarcmplem 31395 frxp2 33394 frxp3 33400 brapply 33870 dfrdg4 33883 ptrest 35388 intima0 40785 elintima 40791 brtrclfv2 40865 |
Copyright terms: Public domain | W3C validator |