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

Theorem imassrn 5512
Description: The image of a class is a subset of its range. Theorem 3.16(xi) of [Monk1] p. 39. (Contributed by NM, 31-Mar-1995.)
Assertion
Ref Expression
imassrn (𝐴𝐵) ⊆ ran 𝐴

Proof of Theorem imassrn
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 exsimpr 1836 . . 3 (∃𝑥(𝑥𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴) → ∃𝑥𝑥, 𝑦⟩ ∈ 𝐴)
21ss2abi 3707 . 2 {𝑦 ∣ ∃𝑥(𝑥𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴)} ⊆ {𝑦 ∣ ∃𝑥𝑥, 𝑦⟩ ∈ 𝐴}
3 dfima3 5504 . 2 (𝐴𝐵) = {𝑦 ∣ ∃𝑥(𝑥𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴)}
4 dfrn3 5344 . 2 ran 𝐴 = {𝑦 ∣ ∃𝑥𝑥, 𝑦⟩ ∈ 𝐴}
52, 3, 43sstr4i 3677 1 (𝐴𝐵) ⊆ ran 𝐴
Colors of variables: wff setvar class
Syntax hints:  wa 383  wex 1744  wcel 2030  {cab 2637  wss 3607  cop 4216  ran crn 5144  cima 5146
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-nul 4822  ax-pr 4936
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ral 2946  df-rex 2947  df-rab 2950  df-v 3233  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-sn 4211  df-pr 4213  df-op 4217  df-br 4686  df-opab 4746  df-xp 5149  df-cnv 5151  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156
This theorem is referenced by:  0ima  5517  cnvimass  5520  fimass  6119  fimacnv  6387  isofrlem  6630  isofr2  6634  f1opw2  6930  imaexg  7145  f1oweALT  7194  frxp  7332  smores2  7496  ecss  7831  f1imaen2g  8058  domunsncan  8101  fopwdom  8109  sbthlem2  8112  sbthlem3  8113  sbthlem5  8115  sbthlem6  8116  ssenen  8175  ssfi  8221  fiint  8278  f1opwfi  8311  marypha1lem  8380  unxpwdom2  8534  tz9.12lem1  8688  acndom2  8915  dfac12lem2  9004  isf34lem5  9238  isf34lem7  9239  isf34lem6  9240  enfin1ai  9244  hsmexlem4  9289  hsmexlem5  9290  fpwwe2lem6  9495  fpwwe2lem9  9498  tskuni  9643  limsupgle  14252  limsupval2  14255  limsupgre  14256  isercolllem2  14440  isercoll  14442  unbenlem  15659  imasless  16247  isacs1i  16365  isacs4lem  17215  mhmima  17410  cntzmhm  17817  f1omvdconj  17912  psgnunilem1  17959  gsumzaddlem  18367  dmdprdd  18444  dprdfeq0  18467  dprdres  18473  dprdss  18474  dprdz  18475  subgdmdprd  18479  dprd2dlem1  18486  dprd2da  18487  dmdprdsplit2lem  18490  lmhmlsp  19097  frlmsslsp  20183  lindff1  20207  lindfrn  20208  f1lindf  20209  lindfmm  20214  lsslindf  20217  cnclsi  21124  cnprest2  21142  paste  21146  cmpfi  21259  connima  21276  1stcfb  21296  1stckgenlem  21404  kgencn3  21409  xkoco1cn  21508  xkoco2cn  21509  xkococnlem  21510  qtopval2  21547  basqtop  21562  imastopn  21571  kqopn  21585  kqcld  21586  hmeontr  21620  hmeores  21622  hmphdis  21647  cmphaushmeo  21651  qtopf1  21667  fbasrn  21735  uzfbas  21749  elfm  21798  elfm3  21801  imaelfm  21802  rnelfm  21804  cnextcn  21918  tgpconncomp  21963  qustgpopn  21970  tsmsf1o  21995  ustimasn  22079  utopbas  22086  restutop  22088  qtopbaslem  22609  tgqioo  22650  cnheiborlem  22800  bndth  22804  fmcfil  23116  ovoliunlem1  23316  volsup  23370  uniioombllem4  23400  uniioombllem5  23401  opnmblALT  23417  volsup2  23419  mbfimaopnlem  23467  mbflimsup  23478  itg2gt0  23572  c1liplem1  23804  dvcnvrelem2  23826  mdegleb  23869  mdeglt  23870  mdegldg  23871  mdegxrcl  23872  mdegcl  23874  ig1peu  23976  efifo  24338  dvlog  24442  efopnlem2  24448  efopn  24449  f1otrg  25796  axcontlem10  25898  htthlem  27902  shsss  28300  imaelshi  29045  pjimai  29163  fimarab  29573  gsummpt2co  29908  sitgclbn  30533  sitgaddlemb  30538  eulerpartlemgvv  30566  eulerpartlemgf  30569  coinfliprv  30672  ballotlemsima  30705  ballotlemro  30712  erdsze2lem2  31312  mrsubrn  31536  msubrn  31552  bdayimaon  31968  nosupbday  31976  noetalem3  31990  noetalem4  31991  nocvxminlem  32018  nocvxmin  32019  tailf  32495  dissneqlem  33317  poimirlem1  33540  poimirlem2  33541  poimirlem3  33542  poimirlem11  33550  poimirlem12  33551  poimirlem15  33554  poimirlem16  33555  poimirlem19  33558  poimirlem30  33569  itg2addnclem2  33592  itg2gt0cn  33595  ftc1anclem7  33621  ftc1anc  33623  ismtyima  33732  ismtyres  33737  heibor1lem  33738  reheibor  33768  elrfirn  37575  isnacs2  37586  isnacs3  37590  fnwe2lem2  37938  lmhmfgima  37971  brtrclfv2  38336  xphe  38392  imo72b2lem0  38782  imo72b2lem2  38784  imo72b2lem1  38788  imo72b2  38792  limccog  40170  liminfval2  40318  mgmhmima  42127
  Copyright terms: Public domain W3C validator