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

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

Proof of Theorem elfvex
StepHypRef Expression
1 elfvdm 6681 . 2 (𝐴 ∈ (𝐹𝐵) → 𝐵 ∈ dom 𝐹)
21elexd 3464 1 (𝐴 ∈ (𝐹𝐵) → 𝐵 ∈ V)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2112  Vcvv 3444  dom cdm 5523  cfv 6328
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773  ax-nul 5177  ax-pow 5234
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2601  df-eu 2632  df-clab 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-ral 3114  df-rex 3115  df-v 3446  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-nul 4247  df-if 4429  df-sn 4529  df-pr 4531  df-op 4535  df-uni 4804  df-br 5034  df-dm 5533  df-iota 6287  df-fv 6336
This theorem is referenced by:  elfvexd  6683  fviss  6720  fiin  8874  elharval  9013  elfzp12  12985  ismre  16856  ismri  16897  isacs  16917  oppccofval  16981  mulgnngsum  18228  gexid  18701  efgrcl  18836  islss  19702  thlle  20389  islbs4  20524  istopon  21520  fgval  22478  fgcl  22486  ufilen  22538  ustssxp  22813  ustbasel  22815  ustincl  22816  ustdiag  22817  ustinvel  22818  ustexhalf  22819  ustfilxp  22821  ustbas2  22834  trust  22838  utopval  22841  elutop  22842  restutop  22846  ustuqtop5  22854  isucn  22887  psmetdmdm  22915  psmetf  22916  psmet0  22918  psmettri2  22919  psmetres2  22924  ismet2  22943  xmetpsmet  22958  metustfbas  23167  metust  23168  iscmet  23891  ulmscl  24977  1vgrex  26798  wlkcompim  27424  clwlkcompim  27572  wwlkbp  27630  2wlkdlem7  27721  clwwlkbp  27773  3wlkdlem7  27954  metidval  31241  pstmval  31246  pstmxmet  31248  issiga  31479  insiga  31504  mvrsval  32860  mrsubcv  32865  mrsubccat  32873  mppsval  32927  topdifinffinlem  34759  istotbnd  35200  isbnd  35211  ismrc  39629  isnacs  39632  mzpcl1  39657  mzpcl2  39658  mzpf  39664  mzpadd  39666  mzpmul  39667  mzpsubmpt  39671  mzpnegmpt  39672  mzpexpmpt  39673  mzpindd  39674  mzpsubst  39676  mzpcompact2  39680  mzpcong  39900  sprel  43988  clintop  44455  assintop  44456  clintopcllaw  44458  assintopcllaw  44459  assintopass  44461
  Copyright terms: Public domain W3C validator