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

Theorem elfvdm 6207
Description: If a function value has a member, the argument belongs to the domain. (Contributed by NM, 12-Feb-2007.)
Assertion
Ref Expression
elfvdm (𝐴 ∈ (𝐹𝐵) → 𝐵 ∈ dom 𝐹)

Proof of Theorem elfvdm
StepHypRef Expression
1 ne0i 3913 . 2 (𝐴 ∈ (𝐹𝐵) → (𝐹𝐵) ≠ ∅)
2 ndmfv 6205 . . 3 𝐵 ∈ dom 𝐹 → (𝐹𝐵) = ∅)
32necon1ai 2818 . 2 ((𝐹𝐵) ≠ ∅ → 𝐵 ∈ dom 𝐹)
41, 3syl 17 1 (𝐴 ∈ (𝐹𝐵) → 𝐵 ∈ dom 𝐹)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1988  wne 2791  c0 3907  dom cdm 5104  cfv 5876
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-8 1990  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600  ax-nul 4780  ax-pow 4834
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-ne 2792  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-uni 4428  df-br 4645  df-dm 5114  df-iota 5839  df-fv 5884
This theorem is referenced by:  elfvex  6208  fveqdmss  6340  eldmrexrnb  6352  elmpt2cl  6861  elovmpt3rab1  6878  mpt2xeldm  7322  mpt2xopn0yelv  7324  mpt2xopxnop0  7326  r1pwss  8632  rankwflemb  8641  r1elwf  8644  rankr1ai  8646  rankdmr1  8649  rankr1ag  8650  rankr1c  8669  r1pwcl  8695  cardne  8776  cardsdomelir  8784  r1wunlim  9544  eluzel2  11677  bitsval  15127  acsfiel  16296  subcrcl  16457  homarcl2  16666  arwrcl  16675  pleval2i  16945  acsdrscl  17151  acsficl  17152  submrcl  17327  gsumws1  17357  issubg  17575  isnsg  17604  cntzrcl  17741  eldprd  18384  isunit  18638  isirred  18680  abvrcl  18802  lbsss  19058  lbssp  19060  lbsind  19061  ply1frcl  19664  elocv  19993  cssi  20009  isobs  20045  linds1  20130  linds2  20131  lindsind  20137  eltg4i  20745  eltg3  20747  tg1  20749  tg2  20750  cldrcl  20811  neiss2  20886  lmrcl  21016  iscnp2  21024  islocfin  21301  kgeni  21321  kqtop  21529  fbasne0  21615  0nelfb  21616  fbsspw  21617  fbasssin  21621  fbun  21625  trfbas2  21628  trfbas  21629  isfil  21632  filss  21638  fbasweak  21650  fgval  21655  elfg  21656  fgcl  21663  isufil  21688  ufilss  21690  trufil  21695  fmval  21728  elfm3  21735  fmfnfmlem4  21742  fmfnfm  21743  elrnust  22009  metflem  22114  xmetf  22115  xmeteq0  22124  xmettri2  22126  xmetres2  22147  blfvalps  22169  blvalps  22171  blval  22172  blfps  22192  blf  22193  isxms2  22234  tmslem  22268  metuval  22335  isphtpc  22774  lmmbr2  23038  lmmbrf  23041  cfili  23047  fmcfil  23051  cfilfcls  23053  iscau2  23056  iscauf  23059  caucfil  23062  cmetcaulem  23067  iscmet3  23072  cfilresi  23074  caussi  23076  causs  23077  metcld2  23086  cmetss  23094  bcthlem1  23102  bcth3  23109  cpncn  23680  cpnres  23681  plybss  23931  tglngne  25426  wlkdlem3  26562  1wlkdlem3  26979  elunirn2  29424  fpwrelmap  29482  metidval  29907  pstmval  29912  brsiga  30220  measbase  30234  cvmsrcl  31220  snmlval  31287  fneuni  32317  uncf  33359  unccur  33363  caures  33527  ismtyval  33570  isismty  33571  heiborlem10  33590  eldiophb  37139  elmnc  37525  issdrg  37586  submgmrcl  41547  elbigofrcl  42109
  Copyright terms: Public domain W3C validator