Theorem elfvdm 6702

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

Step	Hyp	Ref	Expression
1		n0i 4299	. 2 ⊢ (𝐴 ∈ (𝐹‘𝐵) → ¬ (𝐹‘𝐵) = ∅)
2		ndmfv 6700	. 2 ⊢ (¬ 𝐵 ∈ dom 𝐹 → (𝐹‘𝐵) = ∅)
3	1, 2	nsyl2 143	1 ⊢ (𝐴 ∈ (𝐹‘𝐵) → 𝐵 ∈ dom 𝐹)

Syntax hints:   → wi 4   = wceq 1537   ∈ wcel 2114  ∅c0 4291  dom cdm 5555  ‘cfv 6355

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-nul 5210  ax-pow 5266

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3496  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4839  df-br 5067  df-dm 5565  df-iota 6314  df-fv 6363

This theorem is referenced by:  elfvex  6703  elfvmptrab1w  6794  fveqdmss  6846  eldmrexrnb  6858  elmpocl  7387  elovmpt3rab1  7405  mpoxeldm  7877  mpoxopn0yelv  7879  mpoxopxnop0  7881  r1pwss  9213  rankwflemb  9222  r1elwf  9225  rankr1ai  9227  rankdmr1  9230  rankr1ag  9231  rankr1c  9250  r1pwcl  9276  cardne  9394  cardsdomelir  9402  r1wunlim  10159  eluzel2  12249  acsfiel  16925  homarcl2  17295  arwrcl  17304  pleval2i  17574  acsdrscl  17780  acsficl  17781  gsumws1  18002  cntzrcl  18457  smndlsmidm  18781  eldprd  19126  isunit  19407  isirred  19449  lbsss  19849  lbssp  19851  lbsind  19852  ply1frcl  20481  elocv  20812  cssi  20828  linds1  20954  linds2  20955  lindsind  20961  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  23862  lmmbrf  23865  fmcfil  23875  iscau2  23880  iscauf  23883  caucfil  23886  cmetcaulem  23891  iscmet3  23896  cfilresi  23898  caussi  23900  causs  23901  metcld2  23910  cmetss  23919  bcthlem1  23927  bcth3  23934  cpncn  24533  cpnres  24534  tglngne  26336  wlkdlem3  27466  1wlkdlem3  27918  elunirn2  30396  fpwrelmap  30469  metidval  31130  pstmval  31135  brsiga  31442  measbase  31456  cvmsrcl  32511  snmlval  32578  fneuni  33695  uncf  34886  unccur  34890  caures  35050  ismtyval  35093  isismty  35094  heiborlem10  35113  eldiophb  39403  elmnc  39785  submgmrcl  44098  elbigofrcl  44659