Theorem elfvdm 6957

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

Syntax hints:   → wi 4   = wceq 1537   ∈ wcel 2108  ∅c0 4352  dom cdm 5700  ‘cfv 6573

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-nul 5324  ax-pr 5447

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-ral 3068  df-rex 3077  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-dm 5710  df-iota 6525  df-fv 6581

This theorem is referenced by:  elfvex  6958  elfvmptrab1w  7056  fveqdmss  7112  eldmrexrnb  7126  elunirn2OLD  7290  elmpocl  7691  elovmpt3rab1  7710  mpoxeldm  8252  mpoxopn0yelv  8254  mpoxopxnop0  8256  r1pwss  9853  rankwflemb  9862  r1elwf  9865  rankr1ai  9867  rankdmr1  9870  rankr1ag  9871  rankr1c  9890  r1pwcl  9916  cardne  10034  cardsdomelir  10042  r1wunlim  10806  eluzel2  12908  acsfiel  17712  homarcl2  18102  arwrcl  18111  pleval2i  18406  acsdrscl  18616  acsficl  18617  submgmrcl  18733  gsumws1  18873  cntzrcl  19367  smndlsmidm  19698  eldprd  20048  isunit  20399  isirred  20445  lbsss  21099  lbssp  21101  lbsind  21102  elocv  21709  cssi  21725  linds1  21853  linds2  21854  lindsind  21860  ply1frcl  22343  eltg4i  22988  eltg3  22990  tg1  22992  tg2  22993  cldrcl  23055  neiss2  23130  lmrcl  23260  iscnp2  23268  kqtop  23774  fbasne0  23859  0nelfb  23860  fbsspw  23861  fbasssin  23865  fbun  23869  trfbas2  23872  trfbas  23873  isfil  23876  filss  23882  fbasweak  23894  fgval  23899  elfg  23900  fgcl  23907  isufil  23932  ufilss  23934  trufil  23939  fmval  23972  elfm3  23979  fmfnfmlem4  23986  fmfnfm  23987  metflem  24359  xmetf  24360  xmeteq0  24369  xmettri2  24371  xmetres2  24392  blfvalps  24414  blvalps  24416  blval  24417  blfps  24437  blf  24438  isxms2  24479  tmslem  24515  tmslemOLD  24516  lmmbr2  25312  lmmbrf  25315  fmcfil  25325  iscau2  25330  iscauf  25333  caucfil  25336  cmetcaulem  25341  iscmet3  25346  cfilresi  25348  caussi  25350  causs  25351  metcld2  25360  cmetss  25369  bcthlem1  25377  bcth3  25384  cpncn  25992  cpnres  25993  madebdayim  27944  oldbdayim  27945  tglngne  28576  wlkdlem3  29720  1wlkdlem3  30171  fpwrelmap  32747  brsiga  34147  measbase  34161  cvmsrcl  35232  snmlval  35299  fneuni  36313  uncf  37559  unccur  37563  caures  37720  ismtyval  37760  isismty  37761  heiborlem10  37780  eldiophb  42713  elmnc  43093  elbigofrcl  48284