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

Theorem cnvimass 5943
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
StepHypRef Expression
1 imassrn 5934 . 2 (𝐴𝐵) ⊆ ran 𝐴
2 dfdm4 5758 . 2 dom 𝐴 = ran 𝐴
31, 2sseqtrri 4003 1 (𝐴𝐵) ⊆ dom 𝐴
Colors of variables: wff setvar class
Syntax hints:  wss 3935  ccnv 5548  dom cdm 5549  ran crn 5550  cima 5552
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2793  ax-sep 5195  ax-nul 5202  ax-pr 5321
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3497  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-nul 4291  df-if 4466  df-sn 4560  df-pr 4562  df-op 4566  df-br 5059  df-opab 5121  df-xp 5555  df-cnv 5557  df-dm 5559  df-rn 5560  df-res 5561  df-ima 5562
This theorem is referenced by:  fvimacnvi  6815  elpreima  6821  iinpreima  6830  fconst4  6969  frnsuppeq  7833  pw2f1olem  8610  cnvimamptfin  8814  fisuppfi  8830  infxpenlem  9428  enfin2i  9732  fin1a2lem7  9817  smobeth  9997  fpwwe2lem3  10044  fpwwe2lem12  10052  fpwwe2lem13  10053  fpwwe2  10054  canth4  10058  canthwelem  10061  pwfseqlem4  10073  recmulnq  10375  dmrecnq  10379  ltweuz  13319  isercolllem2  15012  isercolllem3  15013  fsumss  15072  ackbijnn  15173  fprodss  15292  1arith  16253  vdwlem1  16307  vdwlem5  16311  vdwlem6  16312  vdwlem8  16314  vdwlem11  16317  ghmpreima  18320  gicer  18356  torsubg  18905  gsumzmhm  18988  gsumzoppg  18995  lmhmpreima  19751  mplcoe5  20179  psr1baslem  20283  evpmss  20660  ofco2  20990  cnpnei  21802  cnclima  21806  iscncl  21807  cnntri  21809  cnclsi  21810  cncls2  21811  cncls  21812  cnntr  21813  cncnp  21818  cnrest2  21824  cndis  21829  2ndcomap  21996  kgencn  22094  kgencn3  22096  ptbasfi  22119  txcnmpt  22162  txdis1cn  22173  qtopval2  22234  basqtop  22249  qtopcld  22251  qtopcn  22252  qtopeu  22254  qtoprest  22255  hmeoimaf1o  22308  hmphtop  22316  hmpher  22322  ordthmeolem  22339  elfm3  22488  rnelfmlem  22490  rnelfm  22491  fmfnfmlem2  22493  fmfnfmlem4  22495  clssubg  22646  tgphaus  22654  qustgplem  22658  ucnprima  22820  ucncn  22823  xmeter  22972  imasf1oxms  23028  metustss  23090  metustexhalf  23095  metustfbas  23096  cfilucfil  23098  metuel2  23104  restmetu  23109  mbfconstlem  24157  i1fima  24208  i1fima2  24209  i1fd  24211  itg1addlem5  24230  plyeq0lem  24729  dgrcl  24752  dgrub  24753  dgrlb  24755  vieta1lem1  24828  vieta1lem2  24829  pserulm  24939  psercn2  24940  psercnlem2  24941  psercnlem1  24942  psercn  24943  pserdvlem1  24944  pserdvlem2  24945  pserdv  24946  pserdv2  24947  abelth  24958  eff1olem  25059  dvlog  25161  logtayl  25170  cxpcn3lem  25255  cxpcn3  25256  resqrtcn  25257  basellem5  25590  elnlfn  29633  nlelshi  29765  xppreima  30323  ofpreima  30339  ofpreima2  30340  fnpreimac  30345  ffsrn  30392  dimkerim  30923  locfinreflem  31004  indpreima  31184  indf1ofs  31185  carsggect  31476  sibfof  31498  sitgclg  31500  eulerpartlemsv2  31516  eulerpartlemsf  31517  eulerpartlemv  31522  eulerpartlemb  31526  eulerpartlemt  31529  eulerpartlemr  31532  eulerpartlemgu  31535  eulerpartlemgs2  31538  eulerpartlemn  31539  cvmliftmolem1  32426  cvmlift2lem9  32456  cvmlift3lem6  32469  cvmlift3lem7  32470  mthmsta  32723  dvtan  34824  itg2addnclem  34825  ftc1anclem6  34854  sstotbnd2  34935  keridl  35193  diaintclN  38076  dibintclN  38185  dihintcl  38362  pw2f1ocnv  39514  dnnumch3lem  39526  dnnumch3  39527  pwfi2f1o  39576  binomcxplemdvbinom  40565  binomcxplemdvsum  40567  binomcxplemnotnn0  40568  wessf1ornlem  41325  sge0f1o  42545  mbfresmf  42897  smfco  42958  smfsuplem1  42966
  Copyright terms: Public domain W3C validator