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

Theorem elfvdm 6681
Description: If a function value has a member, then the argument belongs to the domain. (An artifact of our function value definition.) (Contributed by NM, 12-Feb-2007.) (Proof shortened by BJ, 22-Oct-2022.)
Assertion
Ref Expression
elfvdm (𝐴 ∈ (𝐹𝐵) → 𝐵 ∈ dom 𝐹)

Proof of Theorem elfvdm
StepHypRef Expression
1 n0i 4252 . 2 (𝐴 ∈ (𝐹𝐵) → ¬ (𝐹𝐵) = ∅)
2 ndmfv 6679 . 2 𝐵 ∈ dom 𝐹 → (𝐹𝐵) = ∅)
31, 2nsyl2 143 1 (𝐴 ∈ (𝐹𝐵) → 𝐵 ∈ dom 𝐹)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1538  wcel 2112  c0 4246  dom cdm 5523  cfv 6328
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 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773  ax-nul 5177  ax-pow 5234
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 2601  df-eu 2632  df-clab 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-ral 3114  df-rex 3115  df-v 3446  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-nul 4247  df-if 4429  df-sn 4529  df-pr 4531  df-op 4535  df-uni 4804  df-br 5034  df-dm 5533  df-iota 6287  df-fv 6336
This theorem is referenced by:  elfvex  6682  elfvmptrab1w  6775  fveqdmss  6827  eldmrexrnb  6839  elmpocl  7371  elovmpt3rab1  7389  mpoxeldm  7864  mpoxopn0yelv  7866  mpoxopxnop0  7868  r1pwss  9201  rankwflemb  9210  r1elwf  9213  rankr1ai  9215  rankdmr1  9218  rankr1ag  9219  rankr1c  9238  r1pwcl  9264  cardne  9382  cardsdomelir  9390  r1wunlim  10152  eluzel2  12240  acsfiel  16920  homarcl2  17290  arwrcl  17299  pleval2i  17569  acsdrscl  17775  acsficl  17776  gsumws1  17997  cntzrcl  18452  smndlsmidm  18776  eldprd  19122  isunit  19406  isirred  19448  lbsss  19845  lbssp  19847  lbsind  19848  elocv  20360  cssi  20376  linds1  20502  linds2  20503  lindsind  20509  ply1frcl  20945  eltg4i  21568  eltg3  21570  tg1  21572  tg2  21573  cldrcl  21634  neiss2  21709  lmrcl  21839  iscnp2  21847  kqtop  22353  fbasne0  22438  0nelfb  22439  fbsspw  22440  fbasssin  22444  fbun  22448  trfbas2  22451  trfbas  22452  isfil  22455  filss  22461  fbasweak  22473  fgval  22478  elfg  22479  fgcl  22486  isufil  22511  ufilss  22513  trufil  22518  fmval  22551  elfm3  22558  fmfnfmlem4  22565  fmfnfm  22566  elrnust  22833  metflem  22938  xmetf  22939  xmeteq0  22948  xmettri2  22950  xmetres2  22971  blfvalps  22993  blvalps  22995  blval  22996  blfps  23016  blf  23017  isxms2  23058  tmslem  23092  metuval  23159  lmmbr2  23866  lmmbrf  23869  fmcfil  23879  iscau2  23884  iscauf  23887  caucfil  23890  cmetcaulem  23895  iscmet3  23900  cfilresi  23902  caussi  23904  causs  23905  metcld2  23914  cmetss  23923  bcthlem1  23931  bcth3  23938  cpncn  24542  cpnres  24543  tglngne  26347  wlkdlem3  27477  1wlkdlem3  27927  elunirn2  30417  fpwrelmap  30498  metidval  31241  pstmval  31246  brsiga  31550  measbase  31564  cvmsrcl  32619  snmlval  32686  fneuni  33803  uncf  35029  unccur  35033  caures  35191  ismtyval  35231  isismty  35232  heiborlem10  35251  eldiophb  39685  elmnc  40067  submgmrcl  44389  elbigofrcl  44951
  Copyright terms: Public domain W3C validator