Theorem elfvdm 6866

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  ∅c0 4274  dom cdm 5622  ‘cfv 6490

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-nul 5241  ax-pr 5368

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-dm 5632  df-iota 6446  df-fv 6498

This theorem is referenced by:  elfvex  6867  elfvmptrab1w  6967  fveqdmss  7022  eldmrexrnb  7036  elmpocl  7599  elovmpt3rab1  7618  mpoxeldm  8152  mpoxopn0yelv  8154  mpoxopxnop0  8156  r1pwss  9697  rankwflemb  9706  r1elwf  9709  rankr1ai  9711  rankdmr1  9714  rankr1ag  9715  rankr1c  9734  r1pwcl  9760  cardne  9878  cardsdomelir  9886  r1wunlim  10649  eluzel2  12782  acsfiel  17609  homarcl2  17991  arwrcl  18000  pleval2i  18289  acsdrscl  18501  acsficl  18502  submgmrcl  18652  gsumws1  18795  cntzrcl  19291  smndlsmidm  19620  eldprd  19970  isunit  20342  isirred  20388  lbsss  21062  lbssp  21064  lbsind  21065  elocv  21656  cssi  21672  linds1  21798  linds2  21799  lindsind  21805  ply1frcl  22292  eltg4i  22934  eltg3  22936  tg1  22938  tg2  22939  cldrcl  23000  neiss2  23075  lmrcl  23205  iscnp2  23213  kqtop  23719  fbasne0  23804  0nelfb  23805  fbsspw  23806  fbasssin  23810  fbun  23814  trfbas2  23817  trfbas  23818  isfil  23821  filss  23827  fbasweak  23839  fgval  23844  elfg  23845  fgcl  23852  isufil  23877  ufilss  23879  trufil  23884  fmval  23917  elfm3  23924  fmfnfmlem4  23931  fmfnfm  23932  metflem  24302  xmetf  24303  xmeteq0  24312  xmettri2  24314  xmetres2  24335  blfvalps  24357  blvalps  24359  blval  24360  blfps  24380  blf  24381  isxms2  24422  tmslem  24456  lmmbr2  25235  lmmbrf  25238  fmcfil  25248  iscau2  25253  iscauf  25256  caucfil  25259  cmetcaulem  25264  iscmet3  25269  cfilresi  25271  caussi  25273  causs  25274  metcld2  25283  cmetss  25292  bcthlem1  25300  bcth3  25307  cpncn  25912  cpnres  25913  madebdayim  27899  oldbdayim  27900  newbdayim  27914  cutminmax  27947  tglngne  28637  wlkdlem3  29771  1wlkdlem3  30229  fpwrelmap  32826  brsiga  34348  measbase  34362  r1elcl  35262  cvmsrcl  35467  snmlval  35534  fneuni  36550  uncf  37931  unccur  37935  caures  38092  ismtyval  38132  isismty  38133  heiborlem10  38152  eldiophb  43200  elmnc  43579  elbigofrcl  49023  cicrcl2  49515  cic1st2nd  49519  eloppf  49605