Theorem elfvdm 6877

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  ∅c0 4292  dom cdm 5631  ‘cfv 6499

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 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-nul 5256  ax-pr 5382

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 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-rab 3403  df-v 3446  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5103  df-dm 5641  df-iota 6452  df-fv 6507

This theorem is referenced by:  elfvex  6878  elfvmptrab1w  6977  fveqdmss  7032  eldmrexrnb  7046  elunirn2OLD  7209  elmpocl  7610  elovmpt3rab1  7629  mpoxeldm  8167  mpoxopn0yelv  8169  mpoxopxnop0  8171  r1pwss  9713  rankwflemb  9722  r1elwf  9725  rankr1ai  9727  rankdmr1  9730  rankr1ag  9731  rankr1c  9750  r1pwcl  9776  cardne  9894  cardsdomelir  9902  r1wunlim  10666  eluzel2  12774  acsfiel  17595  homarcl2  17977  arwrcl  17986  pleval2i  18275  acsdrscl  18487  acsficl  18488  submgmrcl  18604  gsumws1  18747  cntzrcl  19241  smndlsmidm  19570  eldprd  19920  isunit  20293  isirred  20339  lbsss  21016  lbssp  21018  lbsind  21019  elocv  21610  cssi  21626  linds1  21752  linds2  21753  lindsind  21759  ply1frcl  22238  eltg4i  22880  eltg3  22882  tg1  22884  tg2  22885  cldrcl  22946  neiss2  23021  lmrcl  23151  iscnp2  23159  kqtop  23665  fbasne0  23750  0nelfb  23751  fbsspw  23752  fbasssin  23756  fbun  23760  trfbas2  23763  trfbas  23764  isfil  23767  filss  23773  fbasweak  23785  fgval  23790  elfg  23791  fgcl  23798  isufil  23823  ufilss  23825  trufil  23830  fmval  23863  elfm3  23870  fmfnfmlem4  23877  fmfnfm  23878  metflem  24249  xmetf  24250  xmeteq0  24259  xmettri2  24261  xmetres2  24282  blfvalps  24304  blvalps  24306  blval  24307  blfps  24327  blf  24328  isxms2  24369  tmslem  24403  lmmbr2  25192  lmmbrf  25195  fmcfil  25205  iscau2  25210  iscauf  25213  caucfil  25216  cmetcaulem  25221  iscmet3  25226  cfilresi  25228  caussi  25230  causs  25231  metcld2  25240  cmetss  25249  bcthlem1  25257  bcth3  25264  cpncn  25871  cpnres  25872  madebdayim  27837  oldbdayim  27838  newbdayim  27852  tglngne  28530  wlkdlem3  29663  1wlkdlem3  30118  fpwrelmap  32706  brsiga  34166  measbase  34180  cvmsrcl  35244  snmlval  35311  fneuni  36328  uncf  37586  unccur  37590  caures  37747  ismtyval  37787  isismty  37788  heiborlem10  37807  eldiophb  42738  elmnc  43118  elbigofrcl  48532  cicrcl2  49025  cic1st2nd  49029  eloppf  49115