Theorem elfvdm 6800

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 4272	. 2 ⊢ (𝐴 ∈ (𝐹‘𝐵) → ¬ (𝐹‘𝐵) = ∅)
2		ndmfv 6798	. 2 ⊢ (¬ 𝐵 ∈ dom 𝐹 → (𝐹‘𝐵) = ∅)
3	1, 2	nsyl2 141	1 ⊢ (𝐴 ∈ (𝐹‘𝐵) → 𝐵 ∈ dom 𝐹)

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2109  ∅c0 4261  dom cdm 5588  ‘cfv 6430

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-10 2140  ax-11 2157  ax-12 2174  ax-ext 2710  ax-sep 5226  ax-nul 5233  ax-pr 5355

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1544  df-fal 1554  df-ex 1786  df-nf 1790  df-sb 2071  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2817  df-ne 2945  df-ral 3070  df-rex 3071  df-rab 3074  df-v 3432  df-dif 3894  df-un 3896  df-in 3898  df-ss 3908  df-nul 4262  df-if 4465  df-sn 4567  df-pr 4569  df-op 4573  df-uni 4845  df-br 5079  df-dm 5598  df-iota 6388  df-fv 6438

This theorem is referenced by:  elfvex  6801  elfvmptrab1w  6895  fveqdmss  6950  eldmrexrnb  6962  elunirn2  7120  elmpocl  7502  elovmpt3rab1  7520  mpoxeldm  8011  mpoxopn0yelv  8013  mpoxopxnop0  8015  r1pwss  9526  rankwflemb  9535  r1elwf  9538  rankr1ai  9540  rankdmr1  9543  rankr1ag  9544  rankr1c  9563  r1pwcl  9589  cardne  9707  cardsdomelir  9715  r1wunlim  10477  eluzel2  12569  acsfiel  17344  homarcl2  17731  arwrcl  17740  pleval2i  18035  acsdrscl  18245  acsficl  18246  gsumws1  18457  cntzrcl  18914  smndlsmidm  19242  eldprd  19588  isunit  19880  isirred  19922  lbsss  20320  lbssp  20322  lbsind  20323  elocv  20854  cssi  20870  linds1  20998  linds2  20999  lindsind  21005  ply1frcl  21465  eltg4i  22091  eltg3  22093  tg1  22095  tg2  22096  cldrcl  22158  neiss2  22233  lmrcl  22363  iscnp2  22371  kqtop  22877  fbasne0  22962  0nelfb  22963  fbsspw  22964  fbasssin  22968  fbun  22972  trfbas2  22975  trfbas  22976  isfil  22979  filss  22985  fbasweak  22997  fgval  23002  elfg  23003  fgcl  23010  isufil  23035  ufilss  23037  trufil  23042  fmval  23075  elfm3  23082  fmfnfmlem4  23089  fmfnfm  23090  elrnust  23357  metflem  23462  xmetf  23463  xmeteq0  23472  xmettri2  23474  xmetres2  23495  blfvalps  23517  blvalps  23519  blval  23520  blfps  23540  blf  23541  isxms2  23582  tmslem  23618  tmslemOLD  23619  metuval  23686  lmmbr2  24404  lmmbrf  24407  fmcfil  24417  iscau2  24422  iscauf  24425  caucfil  24428  cmetcaulem  24433  iscmet3  24438  cfilresi  24440  caussi  24442  causs  24443  metcld2  24452  cmetss  24461  bcthlem1  24469  bcth3  24476  cpncn  25081  cpnres  25082  tglngne  26892  wlkdlem3  28032  1wlkdlem3  28482  fpwrelmap  31047  metidval  31819  pstmval  31824  brsiga  32130  measbase  32144  cvmsrcl  33205  snmlval  33272  madebdayim  34049  oldbdayim  34050  fneuni  34515  uncf  35735  unccur  35739  caures  35897  ismtyval  35937  isismty  35938  heiborlem10  35957  eldiophb  40559  elmnc  40941  submgmrcl  45288  elbigofrcl  45848