Theorem elfvdm 6943

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

Syntax hints:   → wi 4   = wceq 1536   ∈ wcel 2105  ∅c0 4338  dom cdm 5688  ‘cfv 6562

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-nul 5311  ax-pr 5437

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-ral 3059  df-rex 3068  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-dm 5698  df-iota 6515  df-fv 6570

This theorem is referenced by:  elfvex  6944  elfvmptrab1w  7042  fveqdmss  7097  eldmrexrnb  7111  elunirn2OLD  7272  elmpocl  7673  elovmpt3rab1  7692  mpoxeldm  8234  mpoxopn0yelv  8236  mpoxopxnop0  8238  r1pwss  9821  rankwflemb  9830  r1elwf  9833  rankr1ai  9835  rankdmr1  9838  rankr1ag  9839  rankr1c  9858  r1pwcl  9884  cardne  10002  cardsdomelir  10010  r1wunlim  10774  eluzel2  12880  acsfiel  17698  homarcl2  18088  arwrcl  18097  pleval2i  18393  acsdrscl  18603  acsficl  18604  submgmrcl  18720  gsumws1  18863  cntzrcl  19357  smndlsmidm  19688  eldprd  20038  isunit  20389  isirred  20435  lbsss  21093  lbssp  21095  lbsind  21096  elocv  21703  cssi  21719  linds1  21847  linds2  21848  lindsind  21854  ply1frcl  22337  eltg4i  22982  eltg3  22984  tg1  22986  tg2  22987  cldrcl  23049  neiss2  23124  lmrcl  23254  iscnp2  23262  kqtop  23768  fbasne0  23853  0nelfb  23854  fbsspw  23855  fbasssin  23859  fbun  23863  trfbas2  23866  trfbas  23867  isfil  23870  filss  23876  fbasweak  23888  fgval  23893  elfg  23894  fgcl  23901  isufil  23926  ufilss  23928  trufil  23933  fmval  23966  elfm3  23973  fmfnfmlem4  23980  fmfnfm  23981  metflem  24353  xmetf  24354  xmeteq0  24363  xmettri2  24365  xmetres2  24386  blfvalps  24408  blvalps  24410  blval  24411  blfps  24431  blf  24432  isxms2  24473  tmslem  24509  tmslemOLD  24510  lmmbr2  25306  lmmbrf  25309  fmcfil  25319  iscau2  25324  iscauf  25327  caucfil  25330  cmetcaulem  25335  iscmet3  25340  cfilresi  25342  caussi  25344  causs  25345  metcld2  25354  cmetss  25363  bcthlem1  25371  bcth3  25378  cpncn  25986  cpnres  25987  madebdayim  27940  oldbdayim  27941  tglngne  28572  wlkdlem3  29716  1wlkdlem3  30167  fpwrelmap  32750  brsiga  34163  measbase  34177  cvmsrcl  35248  snmlval  35315  fneuni  36329  uncf  37585  unccur  37589  caures  37746  ismtyval  37786  isismty  37787  heiborlem10  37806  eldiophb  42744  elmnc  43124  elbigofrcl  48399