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

Theorem cnvimass 5473
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 5465 . 2 (𝐴𝐵) ⊆ ran 𝐴
2 dfdm4 5305 . 2 dom 𝐴 = ran 𝐴
31, 2sseqtr4i 3630 1 (𝐴𝐵) ⊆ dom 𝐴
Colors of variables: wff setvar class
Syntax hints:  wss 3567  ccnv 5103  dom cdm 5104  ran crn 5105  cima 5107
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600  ax-sep 4772  ax-nul 4780  ax-pr 4897
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-eu 2472  df-mo 2473  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-ral 2914  df-rex 2915  df-rab 2918  df-v 3197  df-dif 3570  df-un 3572  df-in 3574  df-ss 3581  df-nul 3908  df-if 4078  df-sn 4169  df-pr 4171  df-op 4175  df-br 4645  df-opab 4704  df-xp 5110  df-cnv 5112  df-dm 5114  df-rn 5115  df-res 5116  df-ima 5117
This theorem is referenced by:  fvimacnvi  6317  elpreima  6323  iinpreima  6331  fconst4  6463  frnsuppeq  7292  pw2f1olem  8049  cnvimamptfin  8252  fisuppfi  8268  infxpenlem  8821  enfin2i  9128  fin1a2lem7  9213  smobeth  9393  fpwwe2lem3  9440  fpwwe2lem12  9448  fpwwe2lem13  9449  fpwwe2  9450  canth4  9454  canthwelem  9457  pwfseqlem4  9469  recmulnq  9771  dmrecnq  9775  ltweuz  12743  isercolllem2  14377  isercolllem3  14378  fsumss  14437  ackbijnn  14541  fprodss  14659  1arith  15612  vdwlem1  15666  vdwlem5  15670  vdwlem6  15671  vdwlem8  15673  vdwlem11  15676  ghmpreima  17663  gicer  17699  gicerOLD  17700  torsubg  18238  gsumzmhm  18318  gsumzoppg  18325  lmhmpreima  19029  mplcoe5  19449  psr1baslem  19536  evpmss  19913  ofco2  20238  cnpnei  21049  cnclima  21053  iscncl  21054  cnntri  21056  cnclsi  21057  cncls2  21058  cncls  21059  cnntr  21060  cncnp  21065  cnrest2  21071  cndis  21076  2ndcomap  21242  kgencn  21340  kgencn3  21342  ptbasfi  21365  txcnmpt  21408  txdis1cn  21419  qtopval2  21480  basqtop  21495  qtopcld  21497  qtopcn  21498  qtopeu  21500  qtoprest  21501  hmeoimaf1o  21554  hmphtop  21562  hmpher  21568  ordthmeolem  21585  elfm3  21735  rnelfmlem  21737  rnelfm  21738  fmfnfmlem2  21740  fmfnfmlem4  21742  clssubg  21893  tgphaus  21901  qustgplem  21905  ucnprima  22067  ucncn  22070  xmeter  22219  imasf1oxms  22275  metustss  22337  metustexhalf  22342  metustfbas  22343  cfilucfil  22345  metuel2  22351  restmetu  22356  mbfconstlem  23377  i1fima  23426  i1fima2  23427  i1fd  23429  itg1addlem5  23448  plyeq0lem  23947  dgrcl  23970  dgrub  23971  dgrlb  23973  vieta1lem1  24046  vieta1lem2  24047  pserulm  24157  psercn2  24158  psercnlem2  24159  psercnlem1  24160  psercn  24161  pserdvlem1  24162  pserdvlem2  24163  pserdv  24164  pserdv2  24165  abelth  24176  eff1olem  24275  dvlog  24378  logtayl  24387  cxpcn3lem  24469  cxpcn3  24470  resqrtcn  24471  basellem5  24792  elnlfn  28757  nlelshi  28889  xppreima  29422  ofpreima  29439  ofpreima2  29440  ffsrn  29478  locfinreflem  29881  indpreima  30061  indf1ofs  30062  carsggect  30354  sibfof  30376  sitgclg  30378  eulerpartlemsv2  30394  eulerpartlemsf  30395  eulerpartlemv  30400  eulerpartlemb  30404  eulerpartlemt  30407  eulerpartlemr  30410  eulerpartlemgu  30413  eulerpartlemgs2  30416  eulerpartlemn  30417  cvmliftmolem1  31237  cvmlift2lem9  31267  cvmlift3lem6  31280  cvmlift3lem7  31281  mthmsta  31449  dvtan  33431  itg2addnclem  33432  ftc1anclem6  33461  sstotbnd2  33544  keridl  33802  diaintclN  36166  dibintclN  36275  dihintcl  36452  pw2f1ocnv  37423  dnnumch3lem  37435  dnnumch3  37436  pwfi2f1o  37485  binomcxplemdvbinom  38372  binomcxplemdvsum  38374  binomcxplemnotnn0  38375  wessf1ornlem  39187  sge0f1o  40362  mbfresmf  40711  smfco  40772  smfsuplem1  40780
  Copyright terms: Public domain W3C validator