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

Theorem elv 3498
Description: If a proposition is implied by 𝑥 ∈ V (which is true, see vex 3496), then it is true. (Contributed by Peter Mazsa, 13-Oct-2018.)
Hypothesis
Ref Expression
elv.1 (𝑥 ∈ V → 𝜑)
Assertion
Ref Expression
elv 𝜑

Proof of Theorem elv
StepHypRef Expression
1 vex 3496 . 2 𝑥 ∈ V
2 elv.1 . 2 (𝑥 ∈ V → 𝜑)
31, 2ax-mp 5 1 𝜑
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2107  Vcvv 3493
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-ext 2791
This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1774  df-sb 2063  df-clab 2798  df-cleq 2812  df-clel 2891  df-v 3495
This theorem is referenced by:  csbvarg  4381  iinconst  4920  iuniin  4922  iinssiun  4923  iinss1  4925  ssiinf  4969  iinss  4971  iinss2  4972  iinab  4981  iinun2  4986  iundif2  4987  iindif1  4988  iindif2  4990  iinin2  4991  iinpw  5019  brab1  5105  triin  5178  eusvnf  5283  sbcop  5371  pwvabrel  5596  difopab  5695  xpiindi  5699  dmopab2rex  5779  dfima2  5924  args  5950  inisegn0  5954  dffr3  5955  dfse2  5956  dfco2a  6092  iotaval  6322  iinpreima  6830  tfinds2  7570  fvresex  7653  fnse  7819  suppvalbr  7826  cnvimadfsn  7831  reldmtpos  7892  rntpos  7897  ovtpos  7899  dftpos3  7902  tpostpos  7904  wfrlem10  7956  onovuni  7971  oarec  8180  eqerlem  8315  ixpiin  8480  ixpsnf1o  8494  boxriin  8496  idssen  8546  unxpdomlem3  8716  ac6sfi  8754  unbnn2  8767  fifo  8888  inf0  9076  rankxpsuc  9303  tcrank  9305  harcard  9399  infxpenlem  9431  infpwfien  9480  alephcard  9488  dfac3  9539  cflm  9664  fin23lem34  9760  dffin7-2  9812  fin1a2lem13  9826  itunitc1  9834  itunitc  9835  ituniiun  9836  hsmexlem4  9843  fin41  9858  axdclem2  9934  fpwwe2lem12  10055  fpwwe2lem13  10056  fpwwe2  10057  canthwe  10065  pwfseqlem5  10077  axgroth2  10239  axgroth6  10242  grothac  10244  grothtsk  10249  seqfeq4  13411  serle  13417  seqof  13419  hash1snb  13772  hashmap  13788  hashfun  13790  hashbclem  13802  hashf1lem2  13806  hashf1  13807  hash2prde  13820  prprrab  13823  fi1uzind  13847  s3sndisj  14319  s3iunsndisj  14320  rexfiuz  14699  fsumabs  15148  incexclem  15183  fprodcllemf  15304  fprodmodd  15343  iserodd  16164  hashbc0  16333  0ram  16348  ramub1  16356  initoid  17257  termoid  17258  equivestrcsetc  17394  gsumwspan  18003  gsmsymgrfix  18548  symgfixf1  18557  frgpnabllem1  18985  telgsums  19105  opprsubg  19378  subrgpropd  19562  coe1fzgsumdlem  20461  evl1gsumdlem  20511  mdetunilem9  21221  topnex  21596  neitr  21780  ordtbas2  21791  pnfnei  21820  mnfnei  21821  hauscmplem  22006  2ndcsb  22049  2ndcsep  22059  ptpjopn  22212  snfil  22464  fbasrn  22484  rnelfmlem  22552  rnelfm  22553  fmfnfmlem3  22556  fmfnfmlem4  22557  fmfnfm  22558  fclscmp  22630  alexsubALTlem4  22650  ptcmplem2  22653  symgtgp  22706  ustfilxp  22813  restutopopn  22839  ustuqtop2  22843  utopsnneiplem  22848  imasdsf1olem  22975  xpsdsval  22983  metuel2  23167  metustbl  23168  restmetu  23172  xrtgioo  23406  minveclem3b  24023  ovoliunlem1  24095  uniioombllem3  24178  itg1addlem4  24292  dvnff  24512  dvfsumlem3  24617  logfac  25176  gausslemma2dlem1a  25933  umgrislfupgrlem  26899  lfuhgr1v0e  27028  cplgrop  27211  finsumvtxdg2size  27324  rgrusgrprc  27363  elwspths2spth  27738  fusgr2wsp2nb  28105  h2hlm  28749  axhcompl-zf  28767  opsbc2ie  30231  inpr0  30284  iuninc  30304  disjpreima  30326  suppss2f  30376  fnpreimac  30408  tocyccntz  30779  esumpfinvalf  31323  measiuns  31464  bnj23  31976  bnj110  32118  bnj1123  32246  bnj1373  32290  lfuhgr2  32353  lfuhgr3  32354  acycgr1v  32384  umgracycusgr  32389  cusgracyclt3v  32391  dmopab3rexdif  32640  dfpo2  32979  wzel  33099  fprlem2  33126  dfrdg4  33400  bj-sbeq  34206  bj-sbel1  34210  bj-snsetex  34263  bj-snglc  34269  bj-taginv  34286  eldmres  35517  ecres  35522  ecres2  35523  eldmqsres  35530  inxprnres  35536  cnvepres  35542  idinxpss  35557  inxpssidinxp  35560  idinxpssinxp  35561  alrmomorn  35599  alrmomodm  35600  brxrn  35613  dfxrn2  35615  inxpxrn  35630  rnxrn  35633  rnxrnres  35634  rnxrncnvepres  35635  rnxrnidres  35636  1cossres  35661  dfcoels  35662  br1cossinidres  35676  br1cossincnvepres  35677  br1cossxrnidres  35678  br1cossxrncnvepres  35679  refrelcosslem  35689  coss0  35706  cossid  35707  br1cossxrncnvssrres  35735  dfrefrels2  35740  dfcnvrefrels2  35753  dfcnvrefrels3  35754  dfsymrels2  35768  dftrrels2  35798  eldmqs1cossres  35880  dfeldisj5  35941  prter2  36004  cdleme31sdnN  37510  inintabss  39923  inintabd  39924  cnvcnvintabd  39945  cnvintabd  39948  comptiunov2i  40036  cotrcltrcl  40055  corcltrcl  40069  cotrclrcl  40072  rr-grothprimbi  40616  rr-groth  40620  onfrALTlem4VD  41205  iinssiin  41379  iinssf  41391  rnmptpr  41417  wessf1ornlem  41429  rnmptlb  41498  rnmptbddlem  41499  rnmptbd2lem  41504  ellimcabssub0  41882  eusnsn  43246  dfdfat2  43312  onsetreclem1  44792
  Copyright terms: Public domain W3C validator