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

Theorem cnvimass 5916
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 5907 . 2 (𝐴𝐵) ⊆ ran 𝐴
2 dfdm4 5728 . 2 dom 𝐴 = ran 𝐴
31, 2sseqtrri 3952 1 (𝐴𝐵) ⊆ dom 𝐴
Colors of variables: wff setvar class
Syntax hints:  wss 3881  ccnv 5518  dom cdm 5519  ran crn 5520  cima 5522
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5167  ax-nul 5174  ax-pr 5295
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ral 3111  df-rex 3112  df-v 3443  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-nul 4244  df-if 4426  df-sn 4526  df-pr 4528  df-op 4532  df-br 5031  df-opab 5093  df-xp 5525  df-cnv 5527  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532
This theorem is referenced by:  fvimacnvi  6799  elpreima  6805  iinpreima  6814  fconst4  6954  frnsuppeq  7825  pw2f1olem  8604  cnvimamptfin  8809  fisuppfi  8825  infxpenlem  9424  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  13324  isercolllem2  15014  isercolllem3  15015  fsumss  15074  ackbijnn  15175  fprodss  15294  1arith  16253  vdwlem1  16307  vdwlem5  16311  vdwlem6  16312  vdwlem8  16314  vdwlem11  16317  ghmpreima  18372  gicer  18408  torsubg  18967  gsumzmhm  19050  gsumzoppg  19057  lmhmpreima  19813  evpmss  20275  mplcoe5  20708  psr1baslem  20814  ofco2  21056  cnpnei  21869  cnclima  21873  iscncl  21874  cnntri  21876  cnclsi  21877  cncls2  21878  cncls  21879  cnntr  21880  cncnp  21885  cnrest2  21891  cndis  21896  2ndcomap  22063  kgencn  22161  kgencn3  22163  ptbasfi  22186  txcnmpt  22229  txdis1cn  22240  qtopval2  22301  basqtop  22316  qtopcld  22318  qtopcn  22319  qtopeu  22321  qtoprest  22322  hmeoimaf1o  22375  hmphtop  22383  hmpher  22389  ordthmeolem  22406  elfm3  22555  rnelfmlem  22557  rnelfm  22558  fmfnfmlem2  22560  fmfnfmlem4  22562  clssubg  22714  tgphaus  22722  qustgplem  22726  ucnprima  22888  ucncn  22891  xmeter  23040  imasf1oxms  23096  metustss  23158  metustexhalf  23163  metustfbas  23164  cfilucfil  23166  metuel2  23172  restmetu  23177  mbfconstlem  24231  i1fima  24282  i1fima2  24283  i1fd  24285  itg1addlem5  24304  plyeq0lem  24807  dgrcl  24830  dgrub  24831  dgrlb  24833  vieta1lem1  24906  vieta1lem2  24907  pserulm  25017  psercn2  25018  psercnlem2  25019  psercnlem1  25020  psercn  25021  pserdvlem1  25022  pserdvlem2  25023  pserdv  25024  pserdv2  25025  abelth  25036  eff1olem  25140  dvlog  25242  logtayl  25251  cxpcn3lem  25336  cxpcn3  25337  resqrtcn  25338  basellem5  25670  elnlfn  29711  nlelshi  29843  xppreima  30408  ofpreima  30428  ofpreima2  30429  fnpreimac  30434  ffsrn  30491  pwrssmgc  30706  rhmpreimaidl  31011  elrspunidl  31014  dimkerim  31111  locfinreflem  31193  zarcmplem  31234  indpreima  31394  indf1ofs  31395  carsggect  31686  sibfof  31708  sitgclg  31710  eulerpartlemsv2  31726  eulerpartlemsf  31727  eulerpartlemv  31732  eulerpartlemb  31736  eulerpartlemt  31739  eulerpartlemr  31742  eulerpartlemgu  31745  eulerpartlemgs2  31748  eulerpartlemn  31749  cvmliftmolem1  32641  cvmlift2lem9  32671  cvmlift3lem6  32684  cvmlift3lem7  32685  mthmsta  32938  dvtan  35107  itg2addnclem  35108  ftc1anclem6  35135  sstotbnd2  35212  keridl  35470  diaintclN  38354  dibintclN  38463  dihintcl  38640  pw2f1ocnv  39976  dnnumch3lem  39988  dnnumch3  39989  pwfi2f1o  40038  binomcxplemdvbinom  41055  binomcxplemdvsum  41057  binomcxplemnotnn0  41058  wessf1ornlem  41809  sge0f1o  43019  mbfresmf  43371  smfco  43432  smfsuplem1  43440  uniimaprimaeqfv  43897  elsetpreimafvssdm  43901
  Copyright terms: Public domain W3C validator