Theorem elfvdm 6465

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

Syntax hints:   → wi 4   = wceq 1656   ∈ wcel 2164  ∅c0 4144  dom cdm 5342  ‘cfv 6123

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009  ax-6 2075  ax-7 2112  ax-8 2166  ax-9 2173  ax-10 2192  ax-11 2207  ax-12 2220  ax-13 2389  ax-ext 2803  ax-nul 5013  ax-pow 5065

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 879  df-3an 1113  df-tru 1660  df-ex 1879  df-nf 1883  df-sb 2068  df-mo 2605  df-eu 2640  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-ral 3122  df-rex 3123  df-rab 3126  df-v 3416  df-dif 3801  df-un 3803  df-in 3805  df-ss 3812  df-nul 4145  df-if 4307  df-sn 4398  df-pr 4400  df-op 4404  df-uni 4659  df-br 4874  df-dm 5352  df-iota 6086  df-fv 6131

This theorem is referenced by:  elfvex  6467  fveqdmss  6603  eldmrexrnb  6615  elmpt2cl  7136  elovmpt3rab1  7153  mpt2xeldm  7602  mpt2xopn0yelv  7604  mpt2xopxnop0  7606  r1pwss  8924  rankwflemb  8933  r1elwf  8936  rankr1ai  8938  rankdmr1  8941  rankr1ag  8942  rankr1c  8961  r1pwcl  8987  cardne  9104  cardsdomelir  9112  r1wunlim  9874  eluzel2  11973  bitsval  15519  acsfiel  16667  subcrcl  16828  homarcl2  17037  arwrcl  17046  pleval2i  17317  acsdrscl  17523  acsficl  17524  submrcl  17699  gsumws1  17729  issubg  17945  isnsg  17974  cntzrcl  18110  eldprd  18757  isunit  19011  isirred  19053  abvrcl  19177  lbsss  19436  lbssp  19438  lbsind  19439  ply1frcl  20043  elocv  20375  cssi  20391  isobs  20427  linds1  20516  linds2  20517  lindsind  20523  eltg4i  21135  eltg3  21137  tg1  21139  tg2  21140  cldrcl  21201  neiss2  21276  lmrcl  21406  iscnp2  21414  islocfin  21691  kgeni  21711  kqtop  21919  fbasne0  22004  0nelfb  22005  fbsspw  22006  fbasssin  22010  fbun  22014  trfbas2  22017  trfbas  22018  isfil  22021  filss  22027  fbasweak  22039  fgval  22044  elfg  22045  fgcl  22052  isufil  22077  ufilss  22079  trufil  22084  fmval  22117  elfm3  22124  fmfnfmlem4  22131  fmfnfm  22132  elrnust  22398  metflem  22503  xmetf  22504  xmeteq0  22513  xmettri2  22515  xmetres2  22536  blfvalps  22558  blvalps  22560  blval  22561  blfps  22581  blf  22582  isxms2  22623  tmslem  22657  metuval  22724  isphtpc  23163  lmmbr2  23427  lmmbrf  23430  cfili  23436  fmcfil  23440  cfilfcls  23442  iscau2  23445  iscauf  23448  caucfil  23451  cmetcaulem  23456  iscmet3  23461  cfilresi  23463  caussi  23465  causs  23466  metcld2  23475  cmetss  23484  bcthlem1  23492  bcth3  23499  cpncn  24098  cpnres  24099  plybss  24349  tglngne  25862  wlkdlem3  26985  1wlkdlem3  27504  elunirn2  29989  fpwrelmap  30045  metidval  30467  pstmval  30472  brsiga  30780  measbase  30794  cvmsrcl  31781  snmlval  31848  fneuni  32869  uncf  33924  unccur  33928  caures  34091  ismtyval  34134  isismty  34135  heiborlem10  34154  eldiophb  38157  elmnc  38542  issdrg  38603  submgmrcl  42622  elbigofrcl  43184