Theorem elv 3446

Description: If a proposition is implied by 𝑥 ∈ V (which is true, see vex 3444), 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

Step	Hyp	Ref	Expression
1		vex 3444	. 2 ⊢ 𝑥 ∈ V
2		elv.1	. 2 ⊢ (𝑥 ∈ V → 𝜑)
3	1, 2	ax-mp 5	1 ⊢ 𝜑

Syntax hints:   → wi 4   ∈ wcel 2111  Vcvv 3441

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 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443

This theorem is referenced by:  csbvarg  4339  iinconst  4891  iuniin  4893  iinssiun  4894  iinss1  4896  ssiinf  4941  iinss  4943  iinss2  4944  iinab  4953  iinun2  4958  iundif2  4959  iindif1  4960  iindif2  4962  iinin2  4963  iinpw  4991  brab1  5078  triin  5151  eusvnf  5258  sbcop  5345  pwvabrel  5567  difopab  5666  xpiindi  5670  dmopab2rex  5750  dfima2  5898  args  5924  inisegn0  5928  dffr3  5929  dfse2  5930  dfco2a  6066  iotaval  6298  iinpreima  6814  tfinds2  7558  fvresex  7643  fnse  7810  suppvalbr  7817  cnvimadfsn  7822  reldmtpos  7883  rntpos  7888  ovtpos  7890  dftpos3  7893  tpostpos  7895  wfrlem10  7947  onovuni  7962  oarec  8171  eqerlem  8306  ixpiin  8471  ixpsnf1o  8485  boxriin  8487  idssen  8537  unxpdomlem3  8708  ac6sfi  8746  unbnn2  8759  fifo  8880  inf0  9068  rankxpsuc  9295  tcrank  9297  harcard  9391  infxpenlem  9424  infpwfien  9473  alephcard  9481  dfac3  9532  cflm  9661  fin23lem34  9757  dffin7-2  9809  fin1a2lem13  9823  itunitc1  9831  itunitc  9832  ituniiun  9833  hsmexlem4  9840  fin41  9855  axdclem2  9931  fpwwe2lem12  10052  fpwwe2lem13  10053  fpwwe2  10054  canthwe  10062  pwfseqlem5  10074  axgroth2  10236  axgroth6  10239  grothac  10241  grothtsk  10246  seqfeq4  13415  serle  13421  seqof  13423  hash1snb  13776  hashmap  13792  hashfun  13794  hashbclem  13806  hashf1lem2  13810  hashf1  13811  hash2prde  13824  prprrab  13827  fi1uzind  13851  brfi1indALT  13854  s3sndisj  14318  s3iunsndisj  14319  rexfiuz  14699  fsumabs  15148  incexclem  15183  fprodcllemf  15304  fprodmodd  15343  iserodd  16162  hashbc0  16331  0ram  16346  ramub1  16354  initoid  17257  termoid  17258  equivestrcsetc  17394  gsumwspan  18003  gsmsymgrfix  18548  symgfixf1  18557  frgpnabllem1  18986  telgsums  19106  opprsubg  19382  subrgpropd  19563  coe1fzgsumdlem  20930  evl1gsumdlem  20980  mdetunilem9  21225  topnex  21601  neitr  21785  ordtbas2  21796  pnfnei  21825  mnfnei  21826  hauscmplem  22011  2ndcsb  22054  2ndcsep  22064  ptpjopn  22217  snfil  22469  fbasrn  22489  rnelfmlem  22557  rnelfm  22558  fmfnfmlem3  22561  fmfnfmlem4  22562  fmfnfm  22563  fclscmp  22635  alexsubALTlem4  22655  ptcmplem2  22658  symgtgp  22711  ustfilxp  22818  restutopopn  22844  ustuqtop2  22848  utopsnneiplem  22853  imasdsf1olem  22980  xpsdsval  22988  metuel2  23172  metustbl  23173  restmetu  23177  xrtgioo  23411  minveclem3b  24032  ovoliunlem1  24106  uniioombllem3  24189  itg1addlem4  24303  dvnff  24526  dvfsumlem3  24631  logfac  25192  gausslemma2dlem1a  25949  umgrislfupgrlem  26915  lfuhgr1v0e  27044  cplgrop  27227  finsumvtxdg2size  27340  rgrusgrprc  27379  elwspths2spth  27753  fusgr2wsp2nb  28119  h2hlm  28763  axhcompl-zf  28781  opsbc2ie  30246  inpr0  30304  iuninc  30324  disjpreima  30347  suppss2f  30398  fnpreimac  30434  tocyccntz  30836  zarclsiin  31224  esumpfinvalf  31445  measiuns  31586  bnj23  32098  bnj110  32240  bnj1123  32368  bnj1373  32412  lfuhgr2  32478  lfuhgr3  32479  acycgr1v  32509  umgracycusgr  32514  cusgracyclt3v  32516  dmopab3rexdif  32765  dfpo2  33104  wzel  33224  fprlem2  33251  dfrdg4  33525  bj-sbeq  34342  bj-sbel1  34346  bj-snsetex  34399  bj-snglc  34405  bj-taginv  34422  eldmres  35690  ecres  35695  ecres2  35696  eldmqsres  35703  inxprnres  35709  cnvepres  35715  idinxpss  35730  inxpssidinxp  35733  idinxpssinxp  35734  alrmomorn  35772  alrmomodm  35773  brxrn  35786  dfxrn2  35788  inxpxrn  35803  rnxrn  35806  rnxrnres  35807  rnxrncnvepres  35808  rnxrnidres  35809  1cossres  35834  dfcoels  35835  br1cossinidres  35849  br1cossincnvepres  35850  br1cossxrnidres  35851  br1cossxrncnvepres  35852  refrelcosslem  35862  coss0  35879  cossid  35880  br1cossxrncnvssrres  35908  dfrefrels2  35913  dfcnvrefrels2  35926  dfcnvrefrels3  35927  dfsymrels2  35941  dftrrels2  35971  eldmqs1cossres  36053  dfeldisj5  36114  prter2  36177  cdleme31sdnN  37683  inintabss  40278  inintabd  40279  cnvcnvintabd  40300  cnvintabd  40303  comptiunov2i  40407  cotrcltrcl  40426  corcltrcl  40440  cotrclrcl  40443  rr-grothprimbi  41003  rr-groth  41007  onfrALTlem4VD  41592  iinssiin  41764  iinssf  41775  rnmptpr  41801  wessf1ornlem  41811  disjinfi  41820  rnmptlb  41880  rnmptbddlem  41881  rnmptbd2lem  41886  ellimcabssub0  42259  eusnsn  43618  dfdfat2  43684  onsetreclem1  45234