Theorem elfvdm 6915

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2145  ∅c0 4279  dom cdm 5655  ‘cfv 6535

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732  ax-nul 5263  ax-pr 5398

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-dm 5665  df-iota 6491  df-fv 6543

This theorem is used by:  elfvex  6916  elfvmptrab1w  7017  fveqdmss  7074  eldmrexrnb  7088  elmpocl  7658  elovmpt3rab1  7677  mpoxeldm  8214  mpoxopn0yelv  8216  mpoxopxnop0  8218  uncf  8877  r1pwss  9773  rankwflemb  9782  r1elwf  9785  rankr1ai  9787  rankdmr1  9790  rankr1ag  9791  rankr1c  9810  r1pwcl  9838  cardne  9995  cardsdomelir  10003  r1wunlim  10771  eluzel2  12917  acsfiel  17767  homarcl2  18149  arwrcl  18158  pleval2i  18447  acsdrscl  18659  acsficl  18660  submgmrcl  18823  gsumws1  18973  cntzrcl  19480  smndlsmidm  19809  eldprd  20159  isunit  20542  isirred  20588  lbsss  21291  lbssp  21293  lbsind  21294  elocv  21913  cssi  21929  linds1  22055  linds2  22056  lindsind  22062  ply1frcl  22575  eltg4i  23217  eltg3  23219  tg1  23221  tg2  23222  cldrcl  23283  neiss2  23358  lmrcl  23488  iscnp2  23496  kqtop  24003  fbasne0  24088  0nelfb  24089  fbsspw  24090  fbasssin  24094  fbun  24098  trfbas2  24101  trfbas  24102  isfil  24105  filss  24111  fbasweak  24123  fgval  24128  elfg  24129  fgcl  24136  isufil  24161  ufilss  24163  trufil  24168  fmval  24201  elfm3  24208  fmfnfmlem4  24215  fmfnfm  24216  metflem  24586  xmetf  24587  xmeteq0  24596  xmettri2  24598  xmetres2  24619  blfvalps  24641  blvalps  24643  blval  24644  blfps  24664  blf  24665  isxms2  24706  tmslem  24740  lmmbr2  25519  lmmbrf  25522  fmcfil  25532  iscau2  25537  iscauf  25540  caucfil  25543  cmetcaulem  25548  iscmet3  25553  cfilresi  25555  caussi  25557  causs  25558  metcld2  25567  cmetss  25576  bcthlem1  25584  bcth3  25591  cpncn  26195  cpnres  26196  madebdayim  28185  oldbdayim  28186  newbdayim  28200  cutminmax  28233  tglngne  28924  wlkdlem3  30174  1wlkdlem3  30641  fpwrelmap  33236  brsiga  34727  measbase  34741  r1elcl  35638  cvmsrcl  35926  snmlval  35993  fneuni  37033  unccur  38422  caures  38575  ismtyval  38615  isismty  38616  heiborlem10  38635  eldiophb  43667  elmnc  44042  elbigofrcl  49545  cicrcl2  50034  cic1st2nd  50038  eloppf  50124