Theorem elfvdm 6857

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  ∅c0 4284  dom cdm 5619  ‘cfv 6482

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-nul 5245  ax-pr 5371

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-rab 3395  df-v 3438  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-br 5093  df-dm 5629  df-iota 6438  df-fv 6490

This theorem is referenced by:  elfvex  6858  elfvmptrab1w  6957  fveqdmss  7012  eldmrexrnb  7026  elunirn2OLD  7189  elmpocl  7590  elovmpt3rab1  7609  mpoxeldm  8144  mpoxopn0yelv  8146  mpoxopxnop0  8148  r1pwss  9680  rankwflemb  9689  r1elwf  9692  rankr1ai  9694  rankdmr1  9697  rankr1ag  9698  rankr1c  9717  r1pwcl  9743  cardne  9861  cardsdomelir  9869  r1wunlim  10631  eluzel2  12740  acsfiel  17560  homarcl2  17942  arwrcl  17951  pleval2i  18240  acsdrscl  18452  acsficl  18453  submgmrcl  18569  gsumws1  18712  cntzrcl  19206  smndlsmidm  19535  eldprd  19885  isunit  20258  isirred  20304  lbsss  20981  lbssp  20983  lbsind  20984  elocv  21575  cssi  21591  linds1  21717  linds2  21718  lindsind  21724  ply1frcl  22203  eltg4i  22845  eltg3  22847  tg1  22849  tg2  22850  cldrcl  22911  neiss2  22986  lmrcl  23116  iscnp2  23124  kqtop  23630  fbasne0  23715  0nelfb  23716  fbsspw  23717  fbasssin  23721  fbun  23725  trfbas2  23728  trfbas  23729  isfil  23732  filss  23738  fbasweak  23750  fgval  23755  elfg  23756  fgcl  23763  isufil  23788  ufilss  23790  trufil  23795  fmval  23828  elfm3  23835  fmfnfmlem4  23842  fmfnfm  23843  metflem  24214  xmetf  24215  xmeteq0  24224  xmettri2  24226  xmetres2  24247  blfvalps  24269  blvalps  24271  blval  24272  blfps  24292  blf  24293  isxms2  24334  tmslem  24368  lmmbr2  25157  lmmbrf  25160  fmcfil  25170  iscau2  25175  iscauf  25178  caucfil  25181  cmetcaulem  25186  iscmet3  25191  cfilresi  25193  caussi  25195  causs  25196  metcld2  25205  cmetss  25214  bcthlem1  25222  bcth3  25229  cpncn  25836  cpnres  25837  madebdayim  27802  oldbdayim  27803  newbdayim  27817  tglngne  28495  wlkdlem3  29628  1wlkdlem3  30083  fpwrelmap  32677  brsiga  34156  measbase  34170  cvmsrcl  35247  snmlval  35314  fneuni  36331  uncf  37589  unccur  37593  caures  37750  ismtyval  37790  isismty  37791  heiborlem10  37810  eldiophb  42740  elmnc  43119  elbigofrcl  48545  cicrcl2  49038  cic1st2nd  49042  eloppf  49128