Theorem cnvimass 5183

Description: A preimage under any class is included in the domain of the class. (Contributed by FL, 29-Jan-2007.)

Assertion

Ref	Expression
cnvimass	|- ( `' A " B ) C_ dom A

Proof of Theorem cnvimass

Step	Hyp	Ref	Expression
1		imassrn 5175	. 2 |- ( `' A " B ) C_ ran `' A
2		dfdm4 5022	. 2 |- dom A = ran `' A
3	1, 2	sseqtr4i 3341	1 |- ( `' A " B ) C_ dom A

Syntax hints:   C_ wss 3280   `'ccnv 4836   dom cdm 4837   ran crn 4838   "cima 4840

This theorem is referenced by:  fvimacnvi  5803  elpreima  5809  iinpreima  5819  fconst4  5915  pw2f1olem  7171  wemapso2  7477  cantnfcl  7578  cantnfle  7582  cantnflt  7583  cantnff  7585  cantnfp1lem2  7591  cantnfp1lem3  7592  cantnflem1b  7598  cantnflem1d  7600  cantnflem1  7601  cantnflem3  7603  cnfcomlem  7612  cnfcom  7613  cnfcom2lem  7614  cnfcom3lem  7616  cnfcom3  7617  infxpenlem  7851  enfin2i  8157  fin1a2lem7  8242  smobeth  8417  fpwwe2lem3  8464  fpwwe2lem12  8472  fpwwe2lem13  8473  fpwwe2  8474  canth4  8478  canthwelem  8481  pwfseqlem4  8493  recmulnq  8797  dmrecnq  8801  nn0supp  10229  ltweuz  11256  isercolllem2  12414  isercolllem3  12415  fsumss  12474  ackbijnn  12562  1arith  13250  vdwlem1  13304  vdwlem5  13308  vdwlem6  13309  vdwlem8  13311  vdwlem11  13314  fisuppfi  14728  ghmpreima  14982  gicer  15018  torsubg  15424  gsumval3  15469  gsumzres  15472  gsumzcl  15473  gsumzf1o  15474  gsumzaddlem  15481  gsumconst  15487  gsumzmhm  15488  gsumzoppg  15494  gsumunsn  15499  gsum2d  15501  dpjidcl  15571  lmhmpreima  16079  psrass1lem  16397  psrass1  16424  psrdi  16425  psrdir  16426  psrcom  16427  psrass23  16428  mplcoe1  16483  mplcoe2  16485  psr1baslem  16538  psropprmul  16587  coe1mul2  16617  gsumfsum  16721  cnpnei  17282  cnclima  17286  iscncl  17287  cnntri  17289  cnclsi  17290  cncls2  17291  cncls  17292  cnntr  17293  cncnp  17298  cnrest2  17304  cndis  17309  2ndcomap  17474  kgencn  17541  kgencn3  17543  ptbasfi  17566  txcnmpt  17609  txdis1cn  17620  qtopval2  17681  basqtop  17696  qtopcld  17698  qtopcn  17699  qtopeu  17701  qtoprest  17702  hmeoimaf1o  17755  hmphtop  17763  hmpher  17769  ordthmeolem  17786  elfm3  17935  rnelfmlem  17937  rnelfm  17938  fmfnfmlem2  17940  fmfnfmlem4  17942  clssubg  18091  tgphaus  18099  divstgplem  18103  tsmsgsum  18121  ucnprima  18265  ucncn  18268  xmeter  18416  imasf1oxms  18472  metustssOLD  18536  metustss  18537  metustexhalfOLD  18546  metustexhalf  18547  metustfbasOLD  18548  metustfbas  18549  cfilucfilOLD  18552  cfilucfil  18553  metuel2  18562  restmetu  18570  mbfconstlem  19474  i1fima  19523  i1fima2  19524  i1fd  19526  itg1addlem5  19545  mdegfval  19938  mdegleb  19940  mdegldg  19942  deg1mul3le  19992  plyeq0lem  20082  dgrcl  20105  dgrub  20106  dgrlb  20108  vieta1lem1  20180  vieta1lem2  20181  pserulm  20291  psercn2  20292  psercnlem2  20293  psercnlem1  20294  psercn  20295  pserdvlem1  20296  pserdvlem2  20297  pserdv  20298  pserdv2  20299  abelth  20310  eff1olem  20403  dvlog  20495  logtayl  20504  cxpcn3lem  20584  cxpcn3  20585  resqrcn  20586  wilthlem2  20805  wilthlem3  20806  basellem5  20820  elnlfn  23384  nlelshi  23516  xppreima  24012  ofpreima  24034  indpreima  24375  indf1ofs  24376  sibfof  24607  sitgclg  24609  cvmliftmolem1  24921  cvmlift2lem9  24951  cvmlift3lem6  24964  cvmlift3lem7  24965  fprodss  25227  itg2addnclem  26155  sstotbnd2  26373  keridl  26532  pw2f1ocnv  26998  dnnumch3lem  27011  dnnumch3  27012  frlmlbs  27117  fsuppeq  27127  pwfi2f1o  27128  diaintclN  31541  dibintclN  31650  dihintcl  31827

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-sep 4290  ax-nul 4298  ax-pr 4363

This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2258  df-mo 2259  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-ral 2671  df-rex 2672  df-rab 2675  df-v 2918  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-nul 3589  df-if 3700  df-sn 3780  df-pr 3781  df-op 3783  df-br 4173  df-opab 4227  df-xp 4843  df-cnv 4845  df-dm 4847  df-rn 4848  df-res 4849  df-ima 4850