Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  imaex Structured version   Visualization version   GIF version

Theorem imaex 7089
 Description: The image of a set is a set. Theorem 3.17 of [Monk1] p. 39. (Contributed by JJ, 24-Sep-2021.)
Hypothesis
Ref Expression
imaex.1 𝐴 ∈ V
Assertion
Ref Expression
imaex (𝐴𝐵) ∈ V

Proof of Theorem imaex
StepHypRef Expression
1 imaex.1 . 2 𝐴 ∈ V
2 imaexg 7088 . 2 (𝐴 ∈ V → (𝐴𝐵) ∈ V)
31, 2ax-mp 5 1 (𝐴𝐵) ∈ V
 Colors of variables: wff setvar class Syntax hints:   ∈ wcel 1988  Vcvv 3195   “ cima 5107 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-8 1990  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600  ax-sep 4772  ax-nul 4780  ax-pr 4897  ax-un 6934 This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-eu 2472  df-mo 2473  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-ral 2914  df-rex 2915  df-rab 2918  df-v 3197  df-dif 3570  df-un 3572  df-in 3574  df-ss 3581  df-nul 3908  df-if 4078  df-sn 4169  df-pr 4171  df-op 4175  df-uni 4428  df-br 4645  df-opab 4704  df-xp 5110  df-cnv 5112  df-dm 5114  df-rn 5115  df-res 5116  df-ima 5117 This theorem is referenced by:  frxp  7272  pw2f1o  8050  ssenen  8119  fiint  8222  fissuni  8256  fipreima  8257  marypha1lem  8324  infxpenlem  8821  ackbij2lem2  9047  enfin2i  9128  fin1a2lem7  9213  fpwwe  9453  canthwelem  9457  tskuni  9590  isacs4lem  17149  gicsubgen  17702  gsumzaddlem  18302  isunit  18638  evpmss  19913  psgnevpmb  19914  ptbasfi  21365  hmphdis  21580  ustuqtop0  22025  utopsnneiplem  22032  neipcfilu  22081  nghmfval  22507  fta1glem2  23907  fta1blem  23909  lgsqrlem4  25055  legval  25460
 Copyright terms: Public domain W3C validator