MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  funfvima2 Structured version   Visualization version   GIF version

Theorem funfvima2 6533
Description: A function's value in an included preimage belongs to the image. (Contributed by NM, 3-Feb-1997.)
Assertion
Ref Expression
funfvima2 ((Fun 𝐹𝐴 ⊆ dom 𝐹) → (𝐵𝐴 → (𝐹𝐵) ∈ (𝐹𝐴)))

Proof of Theorem funfvima2
StepHypRef Expression
1 ssel 3630 . . 3 (𝐴 ⊆ dom 𝐹 → (𝐵𝐴𝐵 ∈ dom 𝐹))
2 funfvima 6532 . . . . . 6 ((Fun 𝐹𝐵 ∈ dom 𝐹) → (𝐵𝐴 → (𝐹𝐵) ∈ (𝐹𝐴)))
32ex 449 . . . . 5 (Fun 𝐹 → (𝐵 ∈ dom 𝐹 → (𝐵𝐴 → (𝐹𝐵) ∈ (𝐹𝐴))))
43com23 86 . . . 4 (Fun 𝐹 → (𝐵𝐴 → (𝐵 ∈ dom 𝐹 → (𝐹𝐵) ∈ (𝐹𝐴))))
54a2d 29 . . 3 (Fun 𝐹 → ((𝐵𝐴𝐵 ∈ dom 𝐹) → (𝐵𝐴 → (𝐹𝐵) ∈ (𝐹𝐴))))
61, 5syl5 34 . 2 (Fun 𝐹 → (𝐴 ⊆ dom 𝐹 → (𝐵𝐴 → (𝐹𝐵) ∈ (𝐹𝐴))))
76imp 444 1 ((Fun 𝐹𝐴 ⊆ dom 𝐹) → (𝐵𝐴 → (𝐹𝐵) ∈ (𝐹𝐴)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  wcel 2030  wss 3607  dom cdm 5143  cima 5146  Fun wfun 5920  cfv 5926
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-nul 4822  ax-pr 4936
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ral 2946  df-rex 2947  df-rab 2950  df-v 3233  df-sbc 3469  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-sn 4211  df-pr 4213  df-op 4217  df-uni 4469  df-br 4686  df-opab 4746  df-id 5053  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-iota 5889  df-fun 5928  df-fn 5929  df-fv 5934
This theorem is referenced by:  resfvresima  6534  fnfvima  6536  f1oweALT  7194  tz7.49  7585  phimullem  15531  mrcuni  16328  frlmsslsp  20183  lindfrn  20208  iscldtop  20947  1stcfb  21296  2ndcomap  21309  rnelfm  21804  fmfnfmlem2  21806  fmfnfmlem4  21808  qtopbaslem  22609  tgqioo  22650  bndth  22804  volsup  23370  dyadmbllem  23413  opnmbllem  23415  itg1addlem4  23511  c1liplem1  23804  dvcnvrelem1  23825  dvcnvrelem2  23826  plyco0  23993  plyaddlem1  24014  plymullem1  24015  dvloglem  24439  logf1o2  24441  efopn  24449  axcontlem10  25898  imaelshi  29045  funimass4f  29565  sitgclg  30532  cvmliftlem3  31395  nocvxminlem  32018  nocvxmin  32019  ivthALT  32455  opnmbllem0  33575  ismtyres  33737  heibor1lem  33738  ismrc  37581  aomclem4  37944  funfvima2d  38786  fnfvimad  39773
  Copyright terms: Public domain W3C validator