Theorem elfvdm 6898

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  ∅c0 4299  dom cdm 5641  ‘cfv 6514

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 2702  ax-nul 5264  ax-pr 5390

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 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-dm 5651  df-iota 6467  df-fv 6522

This theorem is referenced by:  elfvex  6899  elfvmptrab1w  6998  fveqdmss  7053  eldmrexrnb  7067  elunirn2OLD  7230  elmpocl  7633  elovmpt3rab1  7652  mpoxeldm  8193  mpoxopn0yelv  8195  mpoxopxnop0  8197  r1pwss  9744  rankwflemb  9753  r1elwf  9756  rankr1ai  9758  rankdmr1  9761  rankr1ag  9762  rankr1c  9781  r1pwcl  9807  cardne  9925  cardsdomelir  9933  r1wunlim  10697  eluzel2  12805  acsfiel  17622  homarcl2  18004  arwrcl  18013  pleval2i  18302  acsdrscl  18512  acsficl  18513  submgmrcl  18629  gsumws1  18772  cntzrcl  19266  smndlsmidm  19593  eldprd  19943  isunit  20289  isirred  20335  lbsss  20991  lbssp  20993  lbsind  20994  elocv  21584  cssi  21600  linds1  21726  linds2  21727  lindsind  21733  ply1frcl  22212  eltg4i  22854  eltg3  22856  tg1  22858  tg2  22859  cldrcl  22920  neiss2  22995  lmrcl  23125  iscnp2  23133  kqtop  23639  fbasne0  23724  0nelfb  23725  fbsspw  23726  fbasssin  23730  fbun  23734  trfbas2  23737  trfbas  23738  isfil  23741  filss  23747  fbasweak  23759  fgval  23764  elfg  23765  fgcl  23772  isufil  23797  ufilss  23799  trufil  23804  fmval  23837  elfm3  23844  fmfnfmlem4  23851  fmfnfm  23852  metflem  24223  xmetf  24224  xmeteq0  24233  xmettri2  24235  xmetres2  24256  blfvalps  24278  blvalps  24280  blval  24281  blfps  24301  blf  24302  isxms2  24343  tmslem  24377  lmmbr2  25166  lmmbrf  25169  fmcfil  25179  iscau2  25184  iscauf  25187  caucfil  25190  cmetcaulem  25195  iscmet3  25200  cfilresi  25202  caussi  25204  causs  25205  metcld2  25214  cmetss  25223  bcthlem1  25231  bcth3  25238  cpncn  25845  cpnres  25846  madebdayim  27806  oldbdayim  27807  newbdayim  27821  tglngne  28484  wlkdlem3  29619  1wlkdlem3  30075  fpwrelmap  32663  brsiga  34180  measbase  34194  cvmsrcl  35258  snmlval  35325  fneuni  36342  uncf  37600  unccur  37604  caures  37761  ismtyval  37801  isismty  37802  heiborlem10  37821  eldiophb  42752  elmnc  43132  elbigofrcl  48543  cicrcl2  49036  cic1st2nd  49040  eloppf  49126