Theorem cnvimass 5951

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

Assertion

Ref	Expression
cnvimass	⊢ (◡𝐴 “ 𝐵) ⊆ dom 𝐴

Proof of Theorem cnvimass

Step	Hyp	Ref	Expression
1		imassrn 5942	. 2 ⊢ (◡𝐴 “ 𝐵) ⊆ ran ◡𝐴
2		dfdm4 5766	. 2 ⊢ dom 𝐴 = ran ◡𝐴
3	1, 2	sseqtrri 4006	1 ⊢ (◡𝐴 “ 𝐵) ⊆ dom 𝐴

Syntax hints:   ⊆ wss 3938  ^◡ccnv 5556  dom cdm 5557  ran crn 5558   “ cima 5560

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795  ax-sep 5205  ax-nul 5212  ax-pr 5332

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-ral 3145  df-rex 3146  df-rab 3149  df-v 3498  df-dif 3941  df-un 3943  df-in 3945  df-ss 3954  df-nul 4294  df-if 4470  df-sn 4570  df-pr 4572  df-op 4576  df-br 5069  df-opab 5131  df-xp 5563  df-cnv 5565  df-dm 5567  df-rn 5568  df-res 5569  df-ima 5570

This theorem is referenced by:  fvimacnvi  6824  elpreima  6830  iinpreima  6839  fconst4  6979  frnsuppeq  7844  pw2f1olem  8623  cnvimamptfin  8827  fisuppfi  8843  infxpenlem  9441  enfin2i  9745  fin1a2lem7  9830  smobeth  10010  fpwwe2lem3  10057  fpwwe2lem12  10065  fpwwe2lem13  10066  fpwwe2  10067  canth4  10071  canthwelem  10074  pwfseqlem4  10086  recmulnq  10388  dmrecnq  10392  ltweuz  13332  isercolllem2  15024  isercolllem3  15025  fsumss  15084  ackbijnn  15185  fprodss  15304  1arith  16265  vdwlem1  16319  vdwlem5  16323  vdwlem6  16324  vdwlem8  16326  vdwlem11  16329  ghmpreima  18382  gicer  18418  torsubg  18976  gsumzmhm  19059  gsumzoppg  19066  lmhmpreima  19822  mplcoe5  20251  psr1baslem  20355  evpmss  20732  ofco2  21062  cnpnei  21874  cnclima  21878  iscncl  21879  cnntri  21881  cnclsi  21882  cncls2  21883  cncls  21884  cnntr  21885  cncnp  21890  cnrest2  21896  cndis  21901  2ndcomap  22068  kgencn  22166  kgencn3  22168  ptbasfi  22191  txcnmpt  22234  txdis1cn  22245  qtopval2  22306  basqtop  22321  qtopcld  22323  qtopcn  22324  qtopeu  22326  qtoprest  22327  hmeoimaf1o  22380  hmphtop  22388  hmpher  22394  ordthmeolem  22411  elfm3  22560  rnelfmlem  22562  rnelfm  22563  fmfnfmlem2  22565  fmfnfmlem4  22567  clssubg  22719  tgphaus  22727  qustgplem  22731  ucnprima  22893  ucncn  22896  xmeter  23045  imasf1oxms  23101  metustss  23163  metustexhalf  23168  metustfbas  23169  cfilucfil  23171  metuel2  23177  restmetu  23182  mbfconstlem  24230  i1fima  24281  i1fima2  24282  i1fd  24284  itg1addlem5  24303  plyeq0lem  24802  dgrcl  24825  dgrub  24826  dgrlb  24828  vieta1lem1  24901  vieta1lem2  24902  pserulm  25012  psercn2  25013  psercnlem2  25014  psercnlem1  25015  psercn  25016  pserdvlem1  25017  pserdvlem2  25018  pserdv  25019  pserdv2  25020  abelth  25031  eff1olem  25134  dvlog  25236  logtayl  25245  cxpcn3lem  25330  cxpcn3  25331  resqrtcn  25332  basellem5  25664  elnlfn  29707  nlelshi  29839  xppreima  30396  ofpreima  30412  ofpreima2  30413  fnpreimac  30418  ffsrn  30467  dimkerim  31025  locfinreflem  31106  indpreima  31286  indf1ofs  31287  carsggect  31578  sibfof  31600  sitgclg  31602  eulerpartlemsv2  31618  eulerpartlemsf  31619  eulerpartlemv  31624  eulerpartlemb  31628  eulerpartlemt  31631  eulerpartlemr  31634  eulerpartlemgu  31637  eulerpartlemgs2  31640  eulerpartlemn  31641  cvmliftmolem1  32530  cvmlift2lem9  32560  cvmlift3lem6  32573  cvmlift3lem7  32574  mthmsta  32827  dvtan  34944  itg2addnclem  34945  ftc1anclem6  34974  sstotbnd2  35054  keridl  35312  diaintclN  38196  dibintclN  38305  dihintcl  38482  pw2f1ocnv  39641  dnnumch3lem  39653  dnnumch3  39654  pwfi2f1o  39703  binomcxplemdvbinom  40692  binomcxplemdvsum  40694  binomcxplemnotnn0  40695  wessf1ornlem  41452  sge0f1o  42671  mbfresmf  43023  smfco  43084  smfsuplem1  43092  uniimaprimaeqfv  43549  elsetpreimafvssdm  43553