NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  vex GIF version

Theorem vex 2862
Description: All setvar variables are sets (see isset 2863). Theorem 6.8 of [Quine] p. 43. (Contributed by NM, 5-Aug-1993.)
Assertion
Ref Expression
vex x V

Proof of Theorem vex
StepHypRef Expression
1 eqid 2353 . 2 x = x
2 df-v 2861 . . 3 V = {x x = x}
32abeq2i 2460 . 2 (x V ↔ x = x)
41, 3mpbir 200 1 x V
Colors of variables: wff setvar class
Syntax hints:   = wceq 1642   wcel 1710  Vcvv 2859
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 2861
This theorem is referenced by:  isset  2863  ralv  2872  rexv  2873  reuv  2874  rmov  2875  rabab  2876  sbhypf  2904  ceqex  2969  ralab  2997  rexab  2999  moeq3  3013  mo2icl  3015  reu8  3032  sbc2or  3054  csbvarg  3163  csbiebg  3175  sbcnestgf  3183  sbnfc2  3196  nincom  3226  dblcompl  3227  ddif  3398  csbing  3462  dfun2  3490  dfin2  3491  complab  3524  necompl  3544  vn0  3557  eqv  3565  abvor0  3567  sbss  3659  sscon34  3661  csbifg  3690  ifexg  3721  elpwg  3729  dftp2  3772  prnzg  3836  snssg  3844  difprsnss  3846  sneqrg  3874  pwpr  3883  pwtp  3884  pwv  3886  disj5  3890  unipr  3905  uniprg  3906  unisng  3908  elintg  3934  elintrabg  3939  intss1  3941  ssint  3942  intmin  3946  intss  3947  intssuni  3948  intmin4  3955  intab  3956  intun  3958  intpr  3959  intprg  3960  uniintsn  3963  iinconst  3978  iuniin  3979  iinss1  3981  dfiin2g  4000  ssiinf  4015  iinss  4017  iinss2  4018  0iin  4024  iinab  4027  iinun2  4032  iundif2  4033  iindif2  4035  iinin2  4036  iinxprg  4043  iinuni  4049  sspwuni  4051  iinpw  4054  iunpwss  4055  nincompl  4072  ssofss  4076  axprimlem2  4089  ninexg  4097  vvex  4109  unipw  4117  sspwb  4118  pwadjoin  4119  preqr2g  4126  preq12bg  4128  snel1cg  4141  elpw1  4144  snelpw1  4146  0nel1c  4159  eluni1g  4172  elvvk  4207  opkabssvvk  4208  opkelopkabg  4245  otkelins2kg  4253  otkelins3kg  4254  opkelcokg  4261  elp6  4263  opksnelsik  4265  sikss1c1c  4267  opkelimagekg  4271  cnvkxpk  4276  inxpk  4277  ins2kss  4279  ins3kss  4280  imacok  4282  cokrelk  4284  xpkvexg  4285  cnvkexg  4286  p6exg  4290  dfuni12  4291  ssetkex  4294  sikexg  4296  dfimak2  4298  dfpw12  4301  ins2kexg  4305  ins3kexg  4306  dfidk2  4313  dfuni3  4315  dfint3  4318  setswith  4321  ndisjrelk  4323  dfpw2  4327  eqpw1uni  4330  pw1eqadj  4332  uniabio  4349  iotaval  4350  sniota  4369  csbiotag  4371  dfaddc2  4381  dfnnc2  4395  eladdc  4398  0nelsuc  4400  peano2  4403  findsd  4410  nnc0suc  4412  elsuc  4413  addcass  4415  nncaddccl  4419  nnsucelrlem1  4424  nnsucelr  4428  nndisjeq  4429  prepeano4  4451  preaddccan2lem1  4454  ltfinex  4464  ltfintrilem1  4465  ssfin  4470  eqpwrelk  4478  eqpw1relk  4479  ncfinraiselem2  4480  ncfinraise  4481  ncfinlowerlem1  4482  ncfinlower  4483  eqtfinrelk  4486  tfinsuc  4498  evenfinex  4503  oddfinex  4504  evenoddnnnul  4514  evenodddisjlem1  4515  nnadjoinlem1  4519  nnadjoin  4520  nnadjoinpw  4521  nnpweqlem1  4522  srelk  4524  sfindbl  4530  sfintfinlem1  4531  tfinnnlem1  4533  tfinnn  4534  sfinltfin  4535  spfinex  4537  spfinsfincl  4539  vfintle  4546  vfinspsslem1  4550  vfinspss  4551  vfinspclt  4552  vfinncsp  4554  nulnnn  4556  dfphi2  4569  dfop2lem1  4573  dfop2lem2  4574  dfop2  4575  dfproj12  4576  dfproj22  4577  phi11lem1  4595  proj1op  4600  proj2op  4601  copsexg  4607  phialllem1  4616  phialllem2  4617  opeq  4619  csbopabg  4637  brab1  4684  opabid  4695  elopab  4696  opabn0  4716  el1st  4729  br1stg  4730  setconslem1  4731  setconslem2  4732  setconslem3  4733  setconslem4  4734  setconslem6  4736  setconslem7  4737  df1st2  4738  elswap  4740  dfswap2  4741  dfsset2  4743  dfima2  4745  dfco1  4748  dfsi2  4751  epel  4766  dfid3  4768  opeliunxp  4820  raliunxp  4823  ralxpf  4827  xpvv  4843  ssrel  4844  ssopr  4846  br1st  4858  br2nd  4859  opabid2  4861  dmi  4919  csbima12g  4955  resopab  4999  iss  5000  dfres2  5002  imai  5010  intasym  5028  intirr  5029  cnvi  5032  dmsnn0  5064  dmsnopg  5066  cnvsn  5073  rnsnop  5075  coi1  5094  dfcnv2  5100  elxp4  5108  df2nd2  5111  dfxp2  5113  cnviin  5118  dffun2  5119  nfunv  5138  funsn  5147  funcnvuni  5161  fnunsn  5190  iunfopab  5204  fconstg  5251  fun11iun  5305  f1osng  5323  fv3  5341  tz6.12-2  5346  dffn5  5363  fvopabg  5391  fnasrn  5417  fsn  5432  fsng  5433  fnressn  5438  fressnfv  5439  fvi  5442  fvsng  5446  fvclss  5462  abrexco  5463  opbr1st  5501  opbr2nd  5502  dfid4  5503  1stfo  5505  2ndfo  5506  dfdm4  5507  dfrn5  5508  brswap  5509  swapf1o  5511  1st2nd2  5516  funsi  5520  dmep  5524  oprabid  5550  csbovg  5552  dfoprab2  5558  rnoprab  5576  caovmo  5645  oprabid2  5646  mptv  5718  mpt2v  5719  fmpt2x  5730  brsnsi  5773  brsnsi1  5775  trtxp  5781  brtxp  5783  elfix  5787  op1st2nd  5790  otelins2  5791  otelins3  5792  brimage  5793  oqelins4  5794  dmtxp  5802  txpcofun  5803  otsnelsi3  5805  releqel  5807  releqmpt  5808  releqmpt2  5809  fncup  5813  cupex  5816  composefn  5818  composeex  5820  disjex  5823  addcfnex  5824  addcfn  5825  epprc  5827  funsex  5828  elfunsg  5830  fnsex  5832  brfns  5833  qrpprod  5836  brpprod  5839  dmpprod  5840  fncross  5846  crossex  5850  pw1fnex  5852  fnpw1fn  5853  pw1fnf1o  5855  fnfullfunlem1  5856  fvfullfun  5864  domfnex  5870  ranfnex  5871  clos1ex  5876  clos1exg  5877  clos1conn  5879  clos1is  5881  clos1basesucg  5884  dfnnc3  5885  transex  5910  refex  5911  antisymex  5912  connexex  5913  foundex  5914  extex  5915  symex  5916  ider  5943  ssetpov  5944  erref  5959  eqerlem  5960  erdmrn  5965  erth  5968  erdisj  5972  qsexg  5982  qsid  5990  mapexi  6003  mapprc  6004  mapex  6006  fnmap  6007  fnpm  6008  mapval2  6018  mapsspm  6021  mapsspw  6022  map0  6025  mapsn  6026  bren  6030  enex  6031  ensymi  6036  entr  6038  idssen  6040  fundmen  6043  fundmeng  6044  unen  6048  xpsneng  6050  xpcomeng  6053  xpen  6055  xpassenlem  6056  xpassen  6057  enpw1lem1  6061  enpw1  6062  enmap2lem1  6063  enmap2lem2  6064  enmap2lem3  6065  enmap2lem5  6067  enmap1lem1  6069  enmap1lem2  6070  enmap1lem3  6071  enmap1lem5  6073  enpw1pw  6075  enprmaplem1  6076  enprmaplem2  6077  enprmaplem3  6078  enprmaplem4  6079  enprmaplem5  6080  enprmaplem6  6081  nenpw1pwlem1  6084  nenpw1pwlem2  6085  enpw  6087  lecex  6115  ncseqnc  6128  ovmuc  6130  muccl  6132  mucex  6133  muccom  6134  mucass  6135  ncdisjun  6136  1cnc  6139  df1c3g  6141  muc0  6142  mucid1  6143  ncaddccl  6144  peano4nc  6150  ncspw1eu  6159  eqtc  6161  tcdi  6164  ovcelem1  6171  ceexlem1  6173  ceex  6174  ce0addcnnul  6179  ce0nn  6180  ce0nnulb  6182  ceclb  6183  ce0  6190  el2c  6191  sbthlem2  6204  sbthlem3  6205  sbth  6206  dflec2  6210  nc0le1  6216  ce2lt  6220  dflec3  6221  nclenc  6222  lenc  6223  tc11  6228  taddc  6229  letc  6231  ce0t  6232  ce2le  6233  cet  6234  tce2  6236  te0c  6237  ce0lenc1  6239  tlenc1c  6240  tcfnex  6244  nclennlem1  6248  addcdi  6250  muc0or  6252  0lt1c  6258  csucex  6259  nnltp1clem1  6261  addccan2nclem1  6263  addccan2nclem2  6264  nmembers1lem1  6268  nncdiv3lem1  6275  nncdiv3lem2  6276  nnc3n3p1  6278  spacvallem1  6281  spacind  6287  spacis  6288  nchoicelem3  6291  nchoicelem10  6298  nchoicelem11  6299  nchoicelem12  6300  nchoicelem16  6304  nchoicelem18  6306  frecxp  6314  frecxpg  6315  dmfrec  6316  fnfreclem1  6317  fnfreclem2  6318  fnfreclem3  6319  scancan  6331
  Copyright terms: Public domain W3C validator