Theorem elfvdm 6916

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

Syntax hints:   → wi 4   = wceq 1567   ∈ wcel 2149  ∅c0 4294  dom cdm 5662  ‘cfv 6537

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741  ax-nul 5271  ax-pr 5405

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-ne 2965  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-ss 3930  df-nul 4295  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4877  df-br 5114  df-dm 5672  df-iota 6493  df-fv 6545

This theorem is referenced by:  elfvex  6917  elfvmptrab1w  7018  fveqdmss  7074  eldmrexrnb  7088  elmpocl  7652  elovmpt3rab1  7671  mpoxeldm  8207  mpoxopn0yelv  8209  mpoxopxnop0  8211  r1pwss  9756  rankwflemb  9765  r1elwf  9768  rankr1ai  9770  rankdmr1  9773  rankr1ag  9774  rankr1c  9793  r1pwcl  9819  cardne  9951  cardsdomelir  9959  r1wunlim  10722  eluzel2  12867  acsfiel  17710  homarcl2  18092  arwrcl  18101  pleval2i  18390  acsdrscl  18602  acsficl  18603  submgmrcl  18753  gsumws1  18897  cntzrcl  19397  smndlsmidm  19726  eldprd  20076  isunit  20455  isirred  20501  lbsss  21176  lbssp  21178  lbsind  21179  elocv  21787  cssi  21803  linds1  21929  linds2  21930  lindsind  21936  ply1frcl  22447  eltg4i  23086  eltg3  23088  tg1  23090  tg2  23091  cldrcl  23152  neiss2  23227  lmrcl  23357  iscnp2  23365  kqtop  23871  fbasne0  23956  0nelfb  23957  fbsspw  23958  fbasssin  23962  fbun  23966  trfbas2  23969  trfbas  23970  isfil  23973  filss  23979  fbasweak  23991  fgval  23996  elfg  23997  fgcl  24004  isufil  24029  ufilss  24031  trufil  24036  fmval  24069  elfm3  24076  fmfnfmlem4  24083  fmfnfm  24084  metflem  24454  xmetf  24455  xmeteq0  24464  xmettri2  24466  xmetres2  24487  blfvalps  24509  blvalps  24511  blval  24512  blfps  24532  blf  24533  isxms2  24574  tmslem  24608  lmmbr2  25387  lmmbrf  25390  fmcfil  25400  iscau2  25405  iscauf  25408  caucfil  25411  cmetcaulem  25416  iscmet3  25421  cfilresi  25423  caussi  25425  causs  25426  metcld2  25435  cmetss  25444  bcthlem1  25452  bcth3  25459  cpncn  26064  cpnres  26065  madebdayim  28047  oldbdayim  28048  newbdayim  28062  cutminmax  28095  tglngne  28785  wlkdlem3  29973  1wlkdlem3  30431  fpwrelmap  33019  brsiga  34518  measbase  34532  r1elcl  35434  cvmsrcl  35689  snmlval  35756  fneuni  36781  uncf  38172  unccur  38176  caures  38333  ismtyval  38373  isismty  38374  heiborlem10  38393  eldiophb  43414  elmnc  43789  elbigofrcl  49249  cicrcl2  49740  cic1st2nd  49744  eloppf  49830