Theorem vex 2863

Description: All setvar variables are sets (see isset 2864). Theorem 6.8 of [Quine] p. 43. (Contributed by NM, 5-Aug-1993.)

Assertion

Ref	Expression
vex	|- x e. _V

Proof of Theorem vex

Step	Hyp	Ref	Expression
1		eqid 2353	. 2 |- x = x
2		df-v 2862	. . 3 |- _V = {x | x = x}
3	2	eqabri 2461	. 2 |- (x e. _V <-> x = x)
4	1, 3	mpbir 200	1 |- x e. _V

Syntax hints:   = wceq 1642   e. wcel 1710  _Vcvv 2860

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-11 1746  ax-ext 2334

This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1542  df-sb 1649  df-clab 2340  df-cleq 2346  df-clel 2349  df-v 2862

This theorem is referenced by:  isset  2864  ralv  2873  rexv  2874  reuv  2875  rmov  2876  rabab  2877  sbhypf  2905  ceqex  2970  ralab  2998  rexab  3000  moeq3  3014  mo2icl  3016  reu8  3033  sbc2or  3055  csbvarg  3164  csbiebg  3176  sbcnestgf  3184  sbnfc2  3197  nincom  3227  dblcompl  3228  ddif  3399  csbing  3463  dfun2  3491  dfin2  3492  complab  3525  necompl  3545  vn0  3558  eqv  3566  abvor0  3568  sbss  3660  sscon34  3662  csbifg  3691  ifexg  3722  elpwg  3730  dftp2  3773  prnzg  3837  snssg  3845  difprsnss  3847  sneqrg  3875  pwpr  3884  pwtp  3885  pwv  3887  disj5  3891  unipr  3906  uniprg  3907  unisng  3909  elintg  3935  elintrabg  3940  intss1  3942  ssint  3943  intmin  3947  intss  3948  intssuni  3949  intmin4  3956  intab  3957  intun  3959  intpr  3960  intprg  3961  uniintsn  3964  iinconst  3979  iuniin  3980  iinss1  3982  dfiin2g  4001  ssiinf  4016  iinss  4018  iinss2  4019  0iin  4025  iinab  4028  iinun2  4033  iundif2  4034  iindif2  4036  iinin2  4037  iinxprg  4044  iinuni  4050  sspwuni  4052  iinpw  4055  iunpwss  4056  nincompl  4073  ssofss  4077  axprimlem2  4090  ninexg  4098  vvex  4110  unipw  4118  sspwb  4119  pwadjoin  4120  preqr2g  4127  preq12bg  4129  snel1cg  4142  elpw1  4145  snelpw1  4147  0nel1c  4160  eluni1g  4173  elvvk  4208  opkabssvvk  4209  opkelopkabg  4246  otkelins2kg  4254  otkelins3kg  4255  opkelcokg  4262  elp6  4264  opksnelsik  4266  sikss1c1c  4268  opkelimagekg  4272  cnvkxpk  4277  inxpk  4278  ins2kss  4280  ins3kss  4281  imacok  4283  cokrelk  4285  xpkvexg  4286  cnvkexg  4287  p6exg  4291  dfuni12  4292  ssetkex  4295  sikexg  4297  dfimak2  4299  dfpw12  4302  ins2kexg  4306  ins3kexg  4307  dfidk2  4314  dfuni3  4316  dfint3  4319  setswith  4322  ndisjrelk  4324  dfpw2  4328  eqpw1uni  4331  pw1eqadj  4333  uniabio  4350  iotaval  4351  sniota  4370  csbiotag  4372  dfaddc2  4382  dfnnc2  4396  eladdc  4399  0nelsuc  4401  peano2  4404  findsd  4411  nnc0suc  4413  elsuc  4414  addcass  4416  nncaddccl  4420  nnsucelrlem1  4425  nnsucelr  4429  nndisjeq  4430  prepeano4  4452  preaddccan2lem1  4455  ltfinex  4465  ltfintrilem1  4466  ssfin  4471  eqpwrelk  4479  eqpw1relk  4480  ncfinraiselem2  4481  ncfinraise  4482  ncfinlowerlem1  4483  ncfinlower  4484  eqtfinrelk  4487  tfinsuc  4499  evenfinex  4504  oddfinex  4505  evenoddnnnul  4515  evenodddisjlem1  4516  nnadjoinlem1  4520  nnadjoin  4521  nnadjoinpw  4522  nnpweqlem1  4523  srelk  4525  sfindbl  4531  sfintfinlem1  4532  tfinnnlem1  4534  tfinnn  4535  sfinltfin  4536  spfinex  4538  spfinsfincl  4540  vfintle  4547  vfinspsslem1  4551  vfinspss  4552  vfinspclt  4553  vfinncsp  4555  nulnnn  4557  dfphi2  4570  dfop2lem1  4574  dfop2lem2  4575  dfop2  4576  dfproj12  4577  dfproj22  4578  phi11lem1  4596  proj1op  4601  proj2op  4602  copsexg  4608  phialllem1  4617  phialllem2  4618  opeq  4620  csbopabg  4638  brab1  4685  opabid  4696  elopab  4697  opabn0  4717  el1st  4730  br1stg  4731  setconslem1  4732  setconslem2  4733  setconslem3  4734  setconslem4  4735  setconslem6  4737  setconslem7  4738  df1st2  4739  elswap  4741  dfswap2  4742  dfsset2  4744  dfima2  4746  dfco1  4749  dfsi2  4752  epel  4767  dfid3  4769  opeliunxp  4821  raliunxp  4824  ralxpf  4828  xpvv  4844  ssrel  4845  ssopr  4847  br1st  4859  br2nd  4860  opabid2  4862  dmi  4920  csbima12g  4956  resopab  5000  iss  5001  dfres2  5003  imai  5011  intasym  5029  intirr  5030  cnvi  5033  dmsnn0  5065  dmsnopg  5067  cnvsn  5074  rnsnop  5076  coi1  5095  dfcnv2  5101  elxp4  5109  df2nd2  5112  dfxp2  5114  cnviin  5119  dffun2  5120  nfunv  5139  funsn  5148  funcnvuni  5162  fnunsn  5191  iunfopab  5205  fconstg  5252  fun11iun  5306  f1osng  5324  fv3  5342  tz6.12-2  5347  dffn5  5364  fvopabg  5392  fnasrn  5418  fsn  5433  fsng  5434  fnressn  5439  fressnfv  5440  fvi  5443  fvsng  5447  fvclss  5463  abrexco  5464  opbr1st  5502  opbr2nd  5503  dfid4  5504  1stfo  5506  2ndfo  5507  dfdm4  5508  dfrn5  5509  brswap  5510  swapf1o  5512  1st2nd2  5517  funsi  5521  dmep  5525  oprabid  5551  csbovg  5553  dfoprab2  5559  rnoprab  5577  caovmo  5646  oprabid2  5647  mptv  5719  mpt2v  5720  fmpt2x  5731  brsnsi  5774  brsnsi1  5776  trtxp  5782  brtxp  5784  elfix  5788  op1st2nd  5791  otelins2  5792  otelins3  5793  brimage  5794  oqelins4  5795  dmtxp  5803  txpcofun  5804  otsnelsi3  5806  releqel  5808  releqmpt  5809  releqmpt2  5810  fncup  5814  cupex  5817  composefn  5819  composeex  5821  disjex  5824  addcfnex  5825  addcfn  5826  epprc  5828  funsex  5829  elfunsg  5831  fnsex  5833  brfns  5834  qrpprod  5837  brpprod  5840  dmpprod  5841  fncross  5847  crossex  5851  pw1fnex  5853  fnpw1fn  5854  pw1fnf1o  5856  fnfullfunlem1  5857  fvfullfun  5865  domfnex  5871  ranfnex  5872  clos1ex  5877  clos1exg  5878  clos1conn  5880  clos1is  5882  clos1basesucg  5885  dfnnc3  5886  transex  5911  refex  5912  antisymex  5913  connexex  5914  foundex  5915  extex  5916  symex  5917  ider  5944  ssetpov  5945  erref  5960  eqerlem  5961  erdmrn  5966  erth  5969  erdisj  5973  qsexg  5983  qsid  5991  mapexi  6004  mapprc  6005  mapex  6007  fnmap  6008  fnpm  6009  mapval2  6019  mapsspm  6022  mapsspw  6023  map0  6026  mapsn  6027  bren  6031  enex  6032  ensymi  6037  entr  6039  idssen  6041  fundmen  6044  fundmeng  6045  unen  6049  xpsneng  6051  xpcomeng  6054  xpen  6056  xpassenlem  6057  xpassen  6058  enpw1lem1  6062  enpw1  6063  enmap2lem1  6064  enmap2lem2  6065  enmap2lem3  6066  enmap2lem5  6068  enmap1lem1  6070  enmap1lem2  6071  enmap1lem3  6072  enmap1lem5  6074  enpw1pw  6076  enprmaplem1  6077  enprmaplem2  6078  enprmaplem3  6079  enprmaplem4  6080  enprmaplem5  6081  enprmaplem6  6082  nenpw1pwlem1  6085  nenpw1pwlem2  6086  enpw  6088  lecex  6116  ncseqnc  6129  ovmuc  6131  muccl  6133  mucex  6134  muccom  6135  mucass  6136  ncdisjun  6137  1cnc  6140  df1c3g  6142  muc0  6143  mucid1  6144  ncaddccl  6145  peano4nc  6151  ncspw1eu  6160  eqtc  6162  tcdi  6165  ovcelem1  6172  ceexlem1  6174  ceex  6175  ce0addcnnul  6180  ce0nn  6181  ce0nnulb  6183  ceclb  6184  ce0  6191  el2c  6192  sbthlem2  6205  sbthlem3  6206  sbth  6207  dflec2  6211  nc0le1  6217  ce2lt  6221  dflec3  6222  nclenc  6223  lenc  6224  tc11  6229  taddc  6230  letc  6232  ce0t  6233  ce2le  6234  cet  6235  tce2  6237  te0c  6238  ce0lenc1  6240  tlenc1c  6241  tcfnex  6245  nclennlem1  6249  addcdi  6251  muc0or  6253  0lt1c  6259  csucex  6260  nnltp1clem1  6262  addccan2nclem1  6264  addccan2nclem2  6265  nmembers1lem1  6269  nncdiv3lem1  6276  nncdiv3lem2  6277  nnc3n3p1  6279  spacvallem1  6282  spacind  6288  spacis  6289  nchoicelem3  6292  nchoicelem10  6299  nchoicelem11  6300  nchoicelem12  6301  nchoicelem16  6305  nchoicelem18  6307  frecxp  6315  frecxpg  6316  dmfrec  6317  fnfreclem1  6318  fnfreclem2  6319  fnfreclem3  6320  scancan  6332