Theorem elfvdm 6866

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2106  ∅c0 4273  dom cdm 5624  ‘cfv 6483

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2708  ax-nul 5254  ax-pr 5376

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-ral 3063  df-rex 3072  df-rab 3405  df-v 3444  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-nul 4274  df-if 4478  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4857  df-br 5097  df-dm 5634  df-iota 6435  df-fv 6491

This theorem is referenced by:  elfvex  6867  elfvmptrab1w  6961  fveqdmss  7016  eldmrexrnb  7028  elunirn2OLD  7186  elmpocl  7577  elovmpt3rab1  7595  mpoxeldm  8101  mpoxopn0yelv  8103  mpoxopxnop0  8105  r1pwss  9645  rankwflemb  9654  r1elwf  9657  rankr1ai  9659  rankdmr1  9662  rankr1ag  9663  rankr1c  9682  r1pwcl  9708  cardne  9826  cardsdomelir  9834  r1wunlim  10598  eluzel2  12692  acsfiel  17460  homarcl2  17847  arwrcl  17856  pleval2i  18151  acsdrscl  18361  acsficl  18362  gsumws1  18573  cntzrcl  19029  smndlsmidm  19357  eldprd  19701  isunit  19993  isirred  20035  lbsss  20444  lbssp  20446  lbsind  20447  elocv  20978  cssi  20994  linds1  21122  linds2  21123  lindsind  21129  ply1frcl  21589  eltg4i  22215  eltg3  22217  tg1  22219  tg2  22220  cldrcl  22282  neiss2  22357  lmrcl  22487  iscnp2  22495  kqtop  23001  fbasne0  23086  0nelfb  23087  fbsspw  23088  fbasssin  23092  fbun  23096  trfbas2  23099  trfbas  23100  isfil  23103  filss  23109  fbasweak  23121  fgval  23126  elfg  23127  fgcl  23134  isufil  23159  ufilss  23161  trufil  23166  fmval  23199  elfm3  23206  fmfnfmlem4  23213  fmfnfm  23214  metflem  23586  xmetf  23587  xmeteq0  23596  xmettri2  23598  xmetres2  23619  blfvalps  23641  blvalps  23643  blval  23644  blfps  23664  blf  23665  isxms2  23706  tmslem  23742  tmslemOLD  23743  lmmbr2  24528  lmmbrf  24531  fmcfil  24541  iscau2  24546  iscauf  24549  caucfil  24552  cmetcaulem  24557  iscmet3  24562  cfilresi  24564  caussi  24566  causs  24567  metcld2  24576  cmetss  24585  bcthlem1  24593  bcth3  24600  cpncn  25205  cpnres  25206  tglngne  27199  wlkdlem3  28339  1wlkdlem3  28790  fpwrelmap  31353  brsiga  32447  measbase  32461  cvmsrcl  33523  snmlval  33590  madebdayim  34178  oldbdayim  34179  fneuni  34673  uncf  35912  unccur  35916  caures  36074  ismtyval  36114  isismty  36115  heiborlem10  36134  eldiophb  40892  elmnc  41275  submgmrcl  45754  elbigofrcl  46314