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

Theorem elfvex 6183
Description: If a function value has a member, the argument is a set. (Contributed by Mario Carneiro, 6-Nov-2015.)
Assertion
Ref Expression
elfvex (𝐴 ∈ (𝐹𝐵) → 𝐵 ∈ V)

Proof of Theorem elfvex
StepHypRef Expression
1 elfvdm 6182 . 2 (𝐴 ∈ (𝐹𝐵) → 𝐵 ∈ dom 𝐹)
2 elex 3201 . 2 (𝐵 ∈ dom 𝐹𝐵 ∈ V)
31, 2syl 17 1 (𝐴 ∈ (𝐹𝐵) → 𝐵 ∈ V)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1987  Vcvv 3189  dom cdm 5079  cfv 5852
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-nul 4754  ax-pow 4808
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-ral 2912  df-rex 2913  df-rab 2916  df-v 3191  df-dif 3562  df-un 3564  df-in 3566  df-ss 3573  df-nul 3897  df-if 4064  df-sn 4154  df-pr 4156  df-op 4160  df-uni 4408  df-br 4619  df-dm 5089  df-iota 5815  df-fv 5860
This theorem is referenced by:  elfvexd  6184  fviss  6218  fiin  8280  elharval  8420  elfzp12  12368  ismre  16182  ismri  16223  isacs  16244  oppccofval  16308  gexid  17928  efgrcl  18060  islss  18867  thlle  19973  islbs4  20103  istopon  20649  fgval  21597  fgcl  21605  ufilen  21657  ustssxp  21931  ustbasel  21933  ustincl  21934  ustdiag  21935  ustinvel  21936  ustexhalf  21937  ustfilxp  21939  ustbas2  21952  trust  21956  utopval  21959  elutop  21960  restutop  21964  ustuqtop5  21972  isucn  22005  psmetdmdm  22033  psmetf  22034  psmet0  22036  psmettri2  22037  psmetres2  22042  ismet2  22061  xmetpsmet  22076  metustfbas  22285  metust  22286  iscmet  23005  ulmscl  24054  1vgrex  25799  uvtxaisvtx  26193  vtxnbuvtx  26195  uvtxanbgrvtx  26197  uvtxnbgr  26205  wlkcompim  26414  clwlkcompim  26562  wwlkbp  26618  2wlkdlem7  26714  clwwlkbp  26767  3wlkdlem7  26909  metidval  29739  pstmval  29744  pstmxmet  29746  issiga  29979  insiga  30005  mvrsval  31145  mrsubcv  31150  mrsubccat  31158  mppsval  31212  topdifinffinlem  32862  istotbnd  33235  isbnd  33246  ismrc  36779  isnacs  36782  mzpcl1  36807  mzpcl2  36808  mzpf  36814  mzpadd  36816  mzpmul  36817  mzpsubmpt  36821  mzpnegmpt  36822  mzpexpmpt  36823  mzpindd  36824  mzpsubst  36826  mzpcompact2  36830  mzpcong  37054  sprel  41048  clintop  41158  assintop  41159  clintopcllaw  41161  assintopcllaw  41162  assintopass  41164
  Copyright terms: Public domain W3C validator