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

Theorem cnvimass 5444
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 5436 . 2 (𝐴𝐵) ⊆ ran 𝐴
2 dfdm4 5276 . 2 dom 𝐴 = ran 𝐴
31, 2sseqtr4i 3617 1 (𝐴𝐵) ⊆ dom 𝐴
Colors of variables: wff setvar class
Syntax hints:  wss 3555  ccnv 5073  dom cdm 5074  ran crn 5075  cima 5077
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-sep 4741  ax-nul 4749  ax-pr 4867
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ral 2912  df-rex 2913  df-rab 2916  df-v 3188  df-dif 3558  df-un 3560  df-in 3562  df-ss 3569  df-nul 3892  df-if 4059  df-sn 4149  df-pr 4151  df-op 4155  df-br 4614  df-opab 4674  df-xp 5080  df-cnv 5082  df-dm 5084  df-rn 5085  df-res 5086  df-ima 5087
This theorem is referenced by:  fvimacnvi  6287  elpreima  6293  iinpreima  6301  fconst4  6432  frnsuppeq  7252  pw2f1olem  8008  cnvimamptfin  8211  fisuppfi  8227  infxpenlem  8780  enfin2i  9087  fin1a2lem7  9172  smobeth  9352  fpwwe2lem3  9399  fpwwe2lem12  9407  fpwwe2lem13  9408  fpwwe2  9409  canth4  9413  canthwelem  9416  pwfseqlem4  9428  recmulnq  9730  dmrecnq  9734  ltweuz  12700  isercolllem2  14330  isercolllem3  14331  fsumss  14389  ackbijnn  14485  fprodss  14603  1arith  15555  vdwlem1  15609  vdwlem5  15613  vdwlem6  15614  vdwlem8  15616  vdwlem11  15619  ghmpreima  17603  gicer  17639  gicerOLD  17640  torsubg  18178  gsumzmhm  18258  gsumzoppg  18265  lmhmpreima  18967  mplcoe5  19387  psr1baslem  19474  evpmss  19851  ofco2  20176  cnpnei  20978  cnclima  20982  iscncl  20983  cnntri  20985  cnclsi  20986  cncls2  20987  cncls  20988  cnntr  20989  cncnp  20994  cnrest2  21000  cndis  21005  2ndcomap  21171  kgencn  21269  kgencn3  21271  ptbasfi  21294  txcnmpt  21337  txdis1cn  21348  qtopval2  21409  basqtop  21424  qtopcld  21426  qtopcn  21427  qtopeu  21429  qtoprest  21430  hmeoimaf1o  21483  hmphtop  21491  hmpher  21497  ordthmeolem  21514  elfm3  21664  rnelfmlem  21666  rnelfm  21667  fmfnfmlem2  21669  fmfnfmlem4  21671  clssubg  21822  tgphaus  21830  qustgplem  21834  ucnprima  21996  ucncn  21999  xmeter  22148  imasf1oxms  22204  metustss  22266  metustexhalf  22271  metustfbas  22272  cfilucfil  22274  metuel2  22280  restmetu  22285  mbfconstlem  23302  i1fima  23351  i1fima2  23352  i1fd  23354  itg1addlem5  23373  plyeq0lem  23870  dgrcl  23893  dgrub  23894  dgrlb  23896  vieta1lem1  23969  vieta1lem2  23970  pserulm  24080  psercn2  24081  psercnlem2  24082  psercnlem1  24083  psercn  24084  pserdvlem1  24085  pserdvlem2  24086  pserdv  24087  pserdv2  24088  abelth  24099  eff1olem  24198  dvlog  24297  logtayl  24306  cxpcn3lem  24388  cxpcn3  24389  resqrtcn  24390  basellem5  24711  elnlfn  28636  nlelshi  28768  xppreima  29291  ofpreima  29308  ofpreima2  29309  ffsrn  29347  locfinreflem  29689  indpreima  29868  indf1ofs  29869  carsggect  30161  sibfof  30183  sitgclg  30185  eulerpartlemsv2  30201  eulerpartlemsf  30202  eulerpartlemv  30207  eulerpartlemb  30211  eulerpartlemt  30214  eulerpartlemr  30217  eulerpartlemgu  30220  eulerpartlemgs2  30223  eulerpartlemn  30224  cvmliftmolem1  30971  cvmlift2lem9  31001  cvmlift3lem6  31014  cvmlift3lem7  31015  mthmsta  31183  dvtan  33092  itg2addnclem  33093  ftc1anclem6  33122  sstotbnd2  33205  keridl  33463  diaintclN  35827  dibintclN  35936  dihintcl  36113  pw2f1ocnv  37084  dnnumch3lem  37096  dnnumch3  37097  pwfi2f1o  37146  binomcxplemdvbinom  38034  binomcxplemdvsum  38036  binomcxplemnotnn0  38037  wessf1ornlem  38845  sge0f1o  39906  mbfresmf  40255  smfco  40316  smfsuplem1  40324
  Copyright terms: Public domain W3C validator