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

Theorem elex 3460
 Description: If a class is a member of another class, then it is a set. Theorem 6.12 of [Quine] p. 44. (Contributed by NM, 26-May-1993.) (Proof shortened by Andrew Salmon, 8-Jun-2011.)
Assertion
Ref Expression
elex (𝐴𝐵𝐴 ∈ V)

Proof of Theorem elex
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 exsimpl 1869 . 2 (∃𝑥(𝑥 = 𝐴𝑥𝐵) → ∃𝑥 𝑥 = 𝐴)
2 dfclel 2871 . 2 (𝐴𝐵 ↔ ∃𝑥(𝑥 = 𝐴𝑥𝐵))
3 isset 3454 . 2 (𝐴 ∈ V ↔ ∃𝑥 𝑥 = 𝐴)
41, 2, 33imtr4i 295 1 (𝐴𝐵𝐴 ∈ V)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399   = wceq 1538  ∃wex 1781   ∈ wcel 2111  Vcvv 3442 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 3444 This theorem is referenced by:  elexi  3461  elexd  3462  elissetOLD  3463  prcnel  3466  vtoclgf  3514  vtocl2gf  3519  vtocl3gf  3520  vtocl2g  3521  spcimgft  3535  spcgv  3544  spc3egv  3553  elab4g  3620  elrabf  3626  elrab  3630  mob  3658  sbcex  3732  sbcel1v  3788  sbcabel  3809  csbiebt  3859  eldif  3893  elin  3899  ssv  3941  elun  4079  csbnestgfw  4330  sbcco3gw  4333  csbnestgf  4335  sbcco3g  4338  csbco3g  4339  csbvarg  4342  sbccsb2  4345  ifexg  4475  elpwb  4510  pwidb  4523  elpr2g  4552  elpr2OLD  4554  snidb  4563  ifpr  4592  eldifvsn  4693  prnesn  4753  elpreqpr  4760  dfopg  4765  eluni  4807  eliun  4889  csbexg  5182  nvel  5188  class2seteq  5224  axpweq  5234  reusv2lem4  5271  opeqsng  5362  elopab  5383  epelg  5435  opelvvg  5563  opeliunxp2  5677  opelres  5828  imasng  5922  elimasni  5927  iniseg  5931  inisegn0  5932  dmmptg  6068  elon2  6177  ordsssuc2  6254  iota2  6321  fnmptf  6464  fnmpt  6468  fvelimab  6722  mpteqb  6774  fvmptt  6775  fvmptf  6776  fvopab5  6787  fvopab6  6788  fprg  6904  eloprabga  7250  ovmpos  7288  ov2gf  7289  ovmpox  7293  ovmpoga  7294  ovmpt3rab1  7394  brrpssg  7444  sorpssi  7448  unexg  7465  elpwun  7484  ordeleqon  7496  onintrab  7509  sucexg  7518  ordsucelsuc  7530  onzsl  7554  elxp5  7623  offval3  7678  releldm2  7737  fnmpo  7762  mpoexg  7770  mptmpoopabbrd  7774  bropfvvvv  7783  fsplitfpar  7810  suppval  7828  opeliunxp2f  7877  brtpos2  7899  undefval  7943  tfr2b  8033  tz7.49  8082  oeordi  8214  relelec  8335  ecdmn0  8337  mapvalg  8417  pmvalg  8418  elpmg  8423  elixp2  8466  mptelixpg  8500  elixpsn  8502  snmapen  8591  2pwuninel  8674  fival  8878  elfi2  8880  dffi2  8889  elfiun  8896  wemapso2lem  9018  harval  9026  brwdom  9033  fowdom  9037  brwdom2  9039  brwdom3  9048  en2lp  9071  cantnfsuc  9135  rankvalb  9228  rankwflem  9246  rankr1g  9263  r1pwALT  9277  r1rankid  9290  djulcl  9341  djurcl  9342  inlresf  9345  inrresf  9347  djuss  9351  1stinl  9358  2ndinl  9359  1stinr  9360  2ndinr  9361  cardval3  9383  dfac8alem  9458  isacn  9473  numacn  9478  acndom  9480  cardinfima  9526  unialeph  9530  ackbij1lem5  9653  cflm  9679  isf32lem2  9783  isfin1-2  9814  itunifval  9845  numth3  9899  ttukeylem1  9938  cardidg  9977  ondomon  9992  elwina  10115  elina  10116  wuncval  10171  tskmval  10268  eltskm  10272  recmulnq  10393  elnp  10416  elnpi  10417  npomex  10425  elfzp12  13001  seqp1  13399  hashinf  13711  hashxnn0  13715  hashnn0pnf  13718  hashxrcl  13734  prsshashgt1  13787  hashmap  13812  lsw  13927  ccatfval  13936  ccats1alpha  13984  swrdval  14016  pfxval  14046  splval  14124  splcl  14125  revval  14133  reps  14143  s3sndisj  14338  s3iunsndisj  14339  trclfv  14371  relexp0g  14393  relexpsucnnr  14396  relexp1g  14397  limsupcl  14842  limsupval  14843  clim  14863  rlim  14864  hashbcval  16348  isstruct2  16505  strfvnd  16514  setsvalg  16524  setsfun0  16531  setscom  16539  setsid  16550  ressval  16563  ressinbas  16572  restval  16712  pwsval  16771  xpsfrnel2  16849  ismre  16873  oppcval  16995  brssc  17096  rescval  17109  issubc  17117  isfunc  17146  homadm  17312  homacd  17313  uncfval  17496  pltfval  17581  lubfval  17600  glbfval  17613  joinfval  17623  meetfval  17637  p0val  17663  p1val  17664  oduclatb  17766  ipoval  17776  pws0g  17959  frmdval  18028  vrmdfval  18033  efmnd  18047  efmnd2hash  18071  eqgfval  18341  gaid  18442  cntzfval  18463  elsymgbas  18515  symg2hash  18533  pmtrfval  18591  symggen  18611  gexval  18716  lsmfval  18776  pj1fval  18833  frgpval  18897  vrgpfval  18905  dmdprd  19134  dprdw  19146  pws1  19383  pwsmgp  19385  dvdsr  19413  isrim0  19492  lssset  19719  lspfval  19759  islbs  19862  sraval  19962  zlmval  20231  psgnevpmb  20298  ocvfval  20377  cssval  20393  thlval  20406  dsmmval  20445  dsmmbase  20446  frlmval  20459  uvcfval  20495  islinds  20520  ltbval  20749  evlsval  20795  coe1fval  20875  evls1fval  20984  matval  21057  oftpos  21098  dmatval  21138  scmatval  21150  smadiadetglem2  21318  cpmat  21355  mat2pmatfval  21369  cpm2mfval  21395  decpmatval0  21410  pm2mpval  21441  chpmatfval  21476  basdif0  21599  tgval  21601  eltg  21603  eltg2  21604  neipeltop  21775  islp  21786  ordtval  21835  islocfin  22163  txval  22210  qtopval  22341  isfbas  22475  isfildlem  22503  fmval  22589  fmf  22591  isfcls  22655  alexsubb  22692  tsmsfbas  22774  ustval  22849  elutop  22880  isusp  22908  ispsmet  22952  ismet  22971  isxmet  22972  blfvalps  23031  metustel  23198  tngval  23286  elpi1  23691  rrxval  24032  q1peqb  24799  ig1pval  24817  taylfval  24998  ulmval  25019  iscgrg  26350  isismt  26372  legval  26422  ishlg  26440  ishpg  26597  iscgra  26647  isinag  26676  isleag  26685  iseqlg  26705  ttgval  26713  xmstrkgc  26724  cplgr2vpr  27267  vtxdgfval  27301  1loopgrnb0  27336  ewlksfval  27435  wksfval  27443  iswlkg  27447  wwlksnon  27681  wspthsnon  27682  avril1  28292  ispligb  28304  gidval  28339  isvcOLD  28406  0vfval  28433  elunop  29699  rabexgfGS  30313  disjdifprg  30382  disjdifprg2  30383  abfmpunirn  30459  rabfmpunirn  30460  hashgt1  30600  mntoval  30734  tocycval  30849  evpmval  30886  altgnsg  30890  sgnsv  30901  inftmrel  30908  isinftm  30909  resvval  31000  idlsrgval  31117  rprmval  31133  dimval  31155  dimvalfi  31156  smatfval  31214  lmatval  31232  ispcmp  31276  qqhval2  31399  rrhval  31413  xrhval  31435  indv  31447  esumc  31486  esumpad  31490  esumpcvgval  31513  ofcfval3  31537  issiga  31547  baselsiga  31550  sigasspw  31551  issgon  31558  isrnsigau  31562  sigagenval  31575  ispisys2  31588  cldssbrsiga  31622  sxval  31625  ismeas  31634  cnmbfm  31697  mbfmcnt  31702  elcarsg  31739  sitmval  31783  eulerpartlemt0  31803  sseqval  31822  sseqmw  31825  sseqp1  31829  orvcval  31891  orvcval4  31894  ballotlemsv  31943  satf  32779  satfv1lem  32788  satefv  32840  mrexval  32927  mrsubffval  32933  msubffval  32949  mclsval  32989  eldm3  33180  opelco3  33201  elima4  33202  elno  33336  nosupno  33393  noetalem2  33432  nulsslt  33475  nulssgt  33476  oldlim  33547  elfix2  33625  elsingles  33639  fvimage  33652  funpartlem  33663  elaltxp  33696  brcolinear2  33779  ellines  33873  topfneec  33963  topfneec2  33964  fnejoin2  33977  limsucncmpi  34053  findabrcl  34062  bj-ififc  34179  elelb  34488  bj-pwvrelb  34489  bj-sngltag  34570  bj-xtagex  34576  bj-elsnb  34629  bj-epelg  34635  bj-evalval  34641  bj-ismoore  34671  bj-ideqg1  34730  bj-ideqg1ALT  34731  bj-elid6  34736  bj-diagval  34740  bj-eldiag2  34743  finxpreclem1  34957  finxpreclem3  34961  poimirlem17  35225  elghomlem2OLD  35475  isrngo  35486  isdivrngo  35539  cnvepresex  35902  riotasv2d  36404  riotasv3d  36407  lshpset  36425  lsatset  36437  lcvfbr  36467  lflset  36506  lkrfval  36534  lkrval2  36537  islshpkrN  36567  ldualset  36572  cmtfvalN  36657  cvrfval  36715  pats  36732  llnset  36952  lplnset  36976  lvolset  37019  lineset  37185  pointsetN  37188  psubspset  37191  pmapfval  37203  paddfval  37244  pclfvalN  37336  polfvalN  37351  psubclsetN  37383  watfvalN  37439  lhpset  37442  lautset  37529  pautsetN  37545  ldilfset  37555  ltrnfset  37564  dilfsetN  37599  trnfsetN  37602  trlfset  37607  tgrpfset  38191  tendofset  38205  erngfset  38246  erngfset-rN  38254  dvafset  38451  diaffval  38477  dvhfset  38527  docaffvalN  38568  djaffvalN  38580  dibffval  38587  dicffval  38621  dihffval  38677  dochffval  38796  djhffval  38843  lpolsetN  38929  lcdfval  39035  mapdffval  39073  hvmapffval  39205  hdmap1ffval  39242  hdmapffval  39273  hgmapffval  39332  hlhilset  39381  elrfi  39806  nacsfix  39824  mapfzcons2  39831  sbc2rexgOLD  39900  sbc4rexgOLD  39902  setindtrs  40137  wepwso  40158  hbtlem1  40238  hbtlem7  40240  rgspnval  40283  mendval  40298  cnvtrucl0  40495  eliunov2  40551  iunrelexpmin1  40580  iunrelexpmin2  40584  trclfvcom  40595  cnvtrclfv  40596  trclimalb2  40598  trclfvdecomr  40600  gneispacef2  41010  gneispacern2  41013  gneispace0nelrn  41014  addrval  41341  subrval  41342  mulvval  41343  elixpconstg  41896  mptfnd  42046  upbdrech  42105  climf  42432  climf2  42476  liminfval  42569  dvcosre  42722  itgsinexplem1  42764  itgsubsticclem  42785  dmvolss  42795  stoweidlem26  42836  stoweidlem35  42845  stirlinglem14  42897  fourierdlem42  42959  fourierdlem81  42997  fourierdlem89  43005  fourierdlem91  43007  salgenval  43131  elsprel  44160  sprval  44164  prprval  44199  upwlksfval  44531  isupwlkg  44533  intopval  44630  clintopval  44632  assintopval  44633  isrngisom  44688  rngcvalALTV  44753  rnghmsscmap  44766  ringcvalALTV  44799  rhmsscmap  44812  dmatbas  44978  lincop  44983  lcoop  44986  fdivval  45119  blenval  45151  itcoval  45241  itcoval1  45243  itcoval2  45244  itcoval3  45245  itcovalsucov  45248  lines  45311  spheres  45326
 Copyright terms: Public domain W3C validator