Theorem elfvdm 6929

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2107  ∅c0 4323  dom cdm 5677  ‘cfv 6544

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-nul 5307  ax-pr 5428

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-br 5150  df-dm 5687  df-iota 6496  df-fv 6552

This theorem is referenced by:  elfvex  6930  elfvmptrab1w  7025  fveqdmss  7081  eldmrexrnb  7094  elunirn2OLD  7252  elmpocl  7648  elovmpt3rab1  7666  mpoxeldm  8196  mpoxopn0yelv  8198  mpoxopxnop0  8200  r1pwss  9779  rankwflemb  9788  r1elwf  9791  rankr1ai  9793  rankdmr1  9796  rankr1ag  9797  rankr1c  9816  r1pwcl  9842  cardne  9960  cardsdomelir  9968  r1wunlim  10732  eluzel2  12827  acsfiel  17598  homarcl2  17985  arwrcl  17994  pleval2i  18289  acsdrscl  18499  acsficl  18500  gsumws1  18719  cntzrcl  19191  smndlsmidm  19524  eldprd  19874  isunit  20187  isirred  20233  lbsss  20688  lbssp  20690  lbsind  20691  elocv  21221  cssi  21237  linds1  21365  linds2  21366  lindsind  21372  ply1frcl  21837  eltg4i  22463  eltg3  22465  tg1  22467  tg2  22468  cldrcl  22530  neiss2  22605  lmrcl  22735  iscnp2  22743  kqtop  23249  fbasne0  23334  0nelfb  23335  fbsspw  23336  fbasssin  23340  fbun  23344  trfbas2  23347  trfbas  23348  isfil  23351  filss  23357  fbasweak  23369  fgval  23374  elfg  23375  fgcl  23382  isufil  23407  ufilss  23409  trufil  23414  fmval  23447  elfm3  23454  fmfnfmlem4  23461  fmfnfm  23462  metflem  23834  xmetf  23835  xmeteq0  23844  xmettri2  23846  xmetres2  23867  blfvalps  23889  blvalps  23891  blval  23892  blfps  23912  blf  23913  isxms2  23954  tmslem  23990  tmslemOLD  23991  lmmbr2  24776  lmmbrf  24779  fmcfil  24789  iscau2  24794  iscauf  24797  caucfil  24800  cmetcaulem  24805  iscmet3  24810  cfilresi  24812  caussi  24814  causs  24815  metcld2  24824  cmetss  24833  bcthlem1  24841  bcth3  24848  cpncn  25453  cpnres  25454  madebdayim  27383  oldbdayim  27384  tglngne  27832  wlkdlem3  28972  1wlkdlem3  29423  fpwrelmap  31989  brsiga  33212  measbase  33226  cvmsrcl  34286  snmlval  34353  fneuni  35280  uncf  36515  unccur  36519  caures  36676  ismtyval  36716  isismty  36717  heiborlem10  36736  eldiophb  41543  elmnc  41926  submgmrcl  46600  elbigofrcl  47284