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

Theorem elfvdm 6112
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 3876 . 2 (𝐴 ∈ (𝐹𝐵) → (𝐹𝐵) ≠ ∅)
2 ndmfv 6110 . . 3 𝐵 ∈ dom 𝐹 → (𝐹𝐵) = ∅)
32necon1ai 2805 . 2 ((𝐹𝐵) ≠ ∅ → 𝐵 ∈ dom 𝐹)
41, 3syl 17 1 (𝐴 ∈ (𝐹𝐵) → 𝐵 ∈ dom 𝐹)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1976  wne 2776  c0 3870  dom cdm 5025  cfv 5787
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-8 1978  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2229  ax-ext 2586  ax-nul 4709  ax-pow 4761
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2458  df-mo 2459  df-clab 2593  df-cleq 2599  df-clel 2602  df-nfc 2736  df-ne 2778  df-ral 2897  df-rex 2898  df-rab 2901  df-v 3171  df-dif 3539  df-un 3541  df-in 3543  df-ss 3550  df-nul 3871  df-if 4033  df-sn 4122  df-pr 4124  df-op 4128  df-uni 4364  df-br 4575  df-dm 5035  df-iota 5751  df-fv 5795
This theorem is referenced by:  elfvex  6113  fveqdmss  6244  eldmrexrnb  6256  elmpt2cl  6748  elovmpt3rab1  6765  mpt2xeldm  7198  mpt2xopn0yelv  7200  mpt2xopxnop0  7202  r1pwss  8504  rankwflemb  8513  r1elwf  8516  rankr1ai  8518  rankdmr1  8521  rankr1ag  8522  rankr1c  8541  r1pwcl  8567  cardne  8648  cardsdomelir  8656  r1wunlim  9412  eluzel2  11521  bitsval  14927  acsfiel  16081  subcrcl  16242  homarcl2  16451  arwrcl  16460  pleval2i  16730  acsdrscl  16936  acsficl  16937  submrcl  17112  gsumws1  17142  issubg  17360  isnsg  17389  cntzrcl  17526  eldprd  18169  isunit  18423  isirred  18465  abvrcl  18587  lbsss  18841  lbssp  18843  lbsind  18844  ply1frcl  19447  elocv  19770  cssi  19786  isobs  19822  linds1  19907  linds2  19908  lindsind  19914  eltg4i  20514  eltg3  20516  tg1  20518  tg2  20519  cldrcl  20579  neiss2  20654  lmrcl  20784  iscnp2  20792  islocfin  21069  kgeni  21089  kqtop  21297  fbasne0  21383  0nelfb  21384  fbsspw  21385  fbasssin  21389  fbun  21393  trfbas2  21396  trfbas  21397  isfil  21400  filss  21406  fbasweak  21418  fgval  21423  elfg  21424  fgcl  21431  isufil  21456  ufilss  21458  trufil  21463  fmval  21496  elfm3  21503  fmfnfmlem4  21510  fmfnfm  21511  elrnust  21777  metflem  21881  xmetf  21882  xmeteq0  21891  xmettri2  21893  xmetres2  21914  blfvalps  21936  blvalps  21938  blval  21939  blfps  21959  blf  21960  isxms2  22001  tmslem  22035  metuval  22102  isphtpc  22529  lmmbr2  22780  lmmbrf  22783  cfili  22789  fmcfil  22793  cfilfcls  22795  iscau2  22798  iscauf  22801  caucfil  22804  cmetcaulem  22809  iscmet3  22814  cfilresi  22816  caussi  22818  causs  22819  metcld2  22827  cmetss  22835  bcthlem1  22843  bcth3  22850  cpncn  23419  cpnres  23420  plybss  23668  tglngne  25160  2trllemF  25842  constr1trl  25881  elunirn2  28634  fpwrelmap  28699  metidval  29064  pstmval  29069  brsiga  29376  measbase  29390  cvmsrcl  30303  snmlval  30370  fneuni  31315  uncf  32358  unccur  32362  caures  32526  ismtyval  32569  isismty  32570  heiborlem10  32589  eldiophb  36138  elmnc  36525  issdrg  36586  1wlkdlem3  40892  11wlkdlem3  41305  submgmrcl  41571  elbigofrcl  42141
  Copyright terms: Public domain W3C validator