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

Theorem imaex 7612
 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 7611 . 2 (𝐴 ∈ V → (𝐴𝐵) ∈ V)
31, 2ax-mp 5 1 (𝐴𝐵) ∈ V
 Colors of variables: wff setvar class Syntax hints:   ∈ wcel 2107  Vcvv 3499   “ cima 5556 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 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2797  ax-sep 5199  ax-nul 5206  ax-pr 5325  ax-un 7454 This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2619  df-eu 2651  df-clab 2804  df-cleq 2818  df-clel 2897  df-nfc 2967  df-ral 3147  df-rex 3148  df-rab 3151  df-v 3501  df-dif 3942  df-un 3944  df-in 3946  df-ss 3955  df-nul 4295  df-if 4470  df-sn 4564  df-pr 4566  df-op 4570  df-uni 4837  df-br 5063  df-opab 5125  df-xp 5559  df-cnv 5561  df-dm 5563  df-rn 5564  df-res 5565  df-ima 5566 This theorem is referenced by:  frxp  7814  pw2f1o  8614  ssenen  8683  fiint  8787  fissuni  8821  fipreima  8822  marypha1lem  8889  infxpenlem  9431  ackbij2lem2  9654  enfin2i  9735  fin1a2lem7  9820  fpwwe  10060  canthwelem  10064  tskuni  10197  isacs4lem  17770  gicsubgen  18350  gsumzaddlem  18963  isunit  19329  evpmss  20648  psgnevpmb  20649  ptbasfi  22107  hmphdis  22322  ustuqtop0  22766  utopsnneiplem  22773  neipcfilu  22822  nghmfval  23248  qtopbaslem  23284  fta1glem2  24677  fta1blem  24679  lgsqrlem4  25841  legval  26286  evpmval  30703  altgnsg  30707  brapply  33285  dfrdg4  33298  ptrest  34760  intima0  39859  elintima  39865  brtrclfv2  39939
 Copyright terms: Public domain W3C validator