Theorem imaexg 7103

Description: The image of a set is a set. Theorem 3.17 of [Monk1] p. 39. (Contributed by NM, 24-Jul-1995.)

Assertion

Ref	Expression
imaexg	⊢ (𝐴 ∈ 𝑉 → (𝐴 “ 𝐵) ∈ V)

Proof of Theorem imaexg

Step	Hyp	Ref	Expression
1		imassrn 5477	. 2 ⊢ (𝐴 “ 𝐵) ⊆ ran 𝐴
2		rnexg 7098	. 2 ⊢ (𝐴 ∈ 𝑉 → ran 𝐴 ∈ V)
3		ssexg 4804	. 2 ⊢ (((𝐴 “ 𝐵) ⊆ ran 𝐴 ∧ ran 𝐴 ∈ V) → (𝐴 “ 𝐵) ∈ V)
4	1, 2, 3	sylancr 695	1 ⊢ (𝐴 ∈ 𝑉 → (𝐴 “ 𝐵) ∈ V)

Syntax hints:   → wi 4   ∈ wcel 1990  Vcvv 3200   ⊆ wss 3574  ran crn 5115   “ cima 5117

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pr 4906  ax-un 6949

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-opab 4713  df-xp 5120  df-cnv 5122  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127

This theorem is referenced by:  imaex  7104  ecexg  7746  fopwdom  8068  gsumvalx  17270  gsum2dlem1  18369  gsum2dlem2  18370  gsum2d  18371  xkococnlem  21462  qtopval  21498  ustuqtop4  22048  utopsnnei  22053  fmucnd  22096  metustel  22355  metustss  22356  metustfbas  22362  metuel2  22370  psmetutop  22372  restmetu  22375  cnheiborlem  22753  itg2gt0  23527  shsval  28171  nlfnval  28740  ffsrn  29504  gsummpt2co  29780  gsummpt2d  29781  locfinreflem  29907  qqhval  30018  esum2d  30155  mbfmcnt  30330  sitgaddlemb  30410  eulerpartgbij  30434  eulerpartlemgs2  30442  orvcval  30519  coinfliprv  30544  ballotlemrval  30579  ballotlem7  30597  msrval  31435  mthmval  31472  dfrdg2  31701  brapply  32045  dfrdg4  32058  tailval  32368  bj-clex  32952  isbasisrelowl  33206  relowlpssretop  33212  ptrest  33408  lkrval  34375  isnacs3  37273  pw2f1ocnv  37604  pw2f1o2val  37606  lmhmlnmsplit  37657  intima0  37939  elintima  37945  brtrclfv2  38019  frege98  38255  frege110  38267  frege133  38290  binomcxplemnotnn0  38555  imaexi  39415  tgqioo2  39774  sge0f1o  40599  smfco  41009