Theorem elfvdm 6912

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2108  ∅c0 4308  dom cdm 5654  ‘cfv 6530

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 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707  ax-nul 5276  ax-pr 5402

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 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2809  df-ral 3052  df-rex 3061  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-dm 5664  df-iota 6483  df-fv 6538

This theorem is referenced by:  elfvex  6913  elfvmptrab1w  7012  fveqdmss  7067  eldmrexrnb  7081  elunirn2OLD  7244  elmpocl  7646  elovmpt3rab1  7665  mpoxeldm  8208  mpoxopn0yelv  8210  mpoxopxnop0  8212  r1pwss  9796  rankwflemb  9805  r1elwf  9808  rankr1ai  9810  rankdmr1  9813  rankr1ag  9814  rankr1c  9833  r1pwcl  9859  cardne  9977  cardsdomelir  9985  r1wunlim  10749  eluzel2  12855  acsfiel  17664  homarcl2  18046  arwrcl  18055  pleval2i  18344  acsdrscl  18554  acsficl  18555  submgmrcl  18671  gsumws1  18814  cntzrcl  19308  smndlsmidm  19635  eldprd  19985  isunit  20331  isirred  20377  lbsss  21033  lbssp  21035  lbsind  21036  elocv  21626  cssi  21642  linds1  21768  linds2  21769  lindsind  21775  ply1frcl  22254  eltg4i  22896  eltg3  22898  tg1  22900  tg2  22901  cldrcl  22962  neiss2  23037  lmrcl  23167  iscnp2  23175  kqtop  23681  fbasne0  23766  0nelfb  23767  fbsspw  23768  fbasssin  23772  fbun  23776  trfbas2  23779  trfbas  23780  isfil  23783  filss  23789  fbasweak  23801  fgval  23806  elfg  23807  fgcl  23814  isufil  23839  ufilss  23841  trufil  23846  fmval  23879  elfm3  23886  fmfnfmlem4  23893  fmfnfm  23894  metflem  24265  xmetf  24266  xmeteq0  24275  xmettri2  24277  xmetres2  24298  blfvalps  24320  blvalps  24322  blval  24323  blfps  24343  blf  24344  isxms2  24385  tmslem  24419  lmmbr2  25209  lmmbrf  25212  fmcfil  25222  iscau2  25227  iscauf  25230  caucfil  25233  cmetcaulem  25238  iscmet3  25243  cfilresi  25245  caussi  25247  causs  25248  metcld2  25257  cmetss  25266  bcthlem1  25274  bcth3  25281  cpncn  25888  cpnres  25889  madebdayim  27843  oldbdayim  27844  tglngne  28475  wlkdlem3  29610  1wlkdlem3  30066  fpwrelmap  32656  brsiga  34160  measbase  34174  cvmsrcl  35232  snmlval  35299  fneuni  36311  uncf  37569  unccur  37573  caures  37730  ismtyval  37770  isismty  37771  heiborlem10  37790  eldiophb  42727  elmnc  43107  elbigofrcl  48478  cicrcl2  48958  cic1st2nd  48962