Theorem elex 3493

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.

Step	Hyp	Ref	Expression
1		exsimpl 1872	. 2 ⊢ (∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐵) → ∃𝑥 𝑥 = 𝐴)
2		dfclel 2812	. 2 ⊢ (𝐴 ∈ 𝐵 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐵))
3		isset 3488	. 2 ⊢ (𝐴 ∈ V ↔ ∃𝑥 𝑥 = 𝐴)
4	1, 2, 3	3imtr4i 292	1 ⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ V)

Syntax hints:   → wi 4   ∧ wa 397   = wceq 1542  ∃wex 1782   ∈ wcel 2107  Vcvv 3475

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477

This theorem is referenced by:  elexi  3494  elexd  3495  prcnel  3498  vtoclgf  3554  vtocl2gf  3560  vtocl3gf  3561  vtocl2g  3562  vtocl3g  3563  spcimgft  3577  spcgv  3586  spc3egv  3593  elab4g  3672  elrabf  3678  elrab  3682  class2seteq  3699  mob  3712  sbcex  3786  sbcel1v  3847  sbcabel  3871  csbiebt  3922  eldif  3957  elin  3963  ssv  4005  elun  4147  csbnestgfw  4418  sbcco3gw  4421  csbnestgf  4423  sbcco3g  4426  csbco3g  4427  csbvarg  4430  sbccsb2  4433  elpwb  4609  pwidb  4622  elpr2g  4651  elpr2OLD  4653  snidb  4662  ifpr  4694  snssg  4786  eldifvsn  4799  preqsnd  4858  elpreqpr  4866  dfopg  4870  eluni  4910  eliun  5000  csbexg  5309  nvel  5315  axpweq  5347  reusv2lem4  5398  elopab  5526  epelg  5580  opelvvg  5715  opeliunxp2  5836  opelres  5985  imasng  6079  elimasni  6087  iniseg  6093  inisegn0  6094  dmmptg  6238  elon2  6372  ordsssuc2  6452  iota2  6529  fnmptf  6683  fnmpt  6687  fvelimab  6960  mpteqb  7013  fvmptt  7014  fvmptf  7015  fvopab5  7026  fvopab6  7027  fprg  7148  eloprabga  7511  eloprabgaOLD  7512  ovmpos  7551  ov2gf  7552  ovmpox  7556  ovmpoga  7557  ovmpt3rab1  7659  brrpssg  7710  sorpssi  7714  unexg  7731  elpwun  7751  ordeleqon  7764  onintrab  7779  sucexg  7788  sucexeloni  7792  ordsucelsuc  7805  onzsl  7830  dmfexALT  7896  elxp5  7909  offval3  7964  releldm2  8024  fnmpo  8050  mpoexg  8058  mptmpoopabbrdOLD  8064  bropfvvvv  8073  fsplitfpar  8099  suppval  8143  opeliunxp2f  8190  brtpos2  8212  undefval  8256  tfr2b  8391  tz7.49  8440  oeordi  8583  relelec  8744  ecdmn0  8746  mapvalg  8826  pmvalg  8827  elpmg  8833  elixp2  8891  mptelixpg  8925  elixpsn  8927  2pwuninel  9128  rex2dom  9242  fival  9403  elfi2  9405  dffi2  9414  elfiun  9421  wemapso2lem  9543  harval  9551  brwdom  9558  fowdom  9562  brwdom2  9564  brwdom3  9573  en2lp  9597  cantnfsuc  9661  rankvalb  9788  rankwflem  9806  rankr1g  9823  r1pwALT  9837  r1rankid  9850  djulcl  9901  djurcl  9902  inlresf  9905  inrresf  9907  djuss  9911  1stinl  9918  2ndinl  9919  1stinr  9920  2ndinr  9921  cardval3  9943  dfac8alem  10020  isacn  10035  numacn  10040  acndom  10042  cardinfima  10088  unialeph  10092  ackbij1lem5  10215  cflm  10241  isf32lem2  10345  isfin1-2  10376  itunifval  10407  numth3  10461  ttukeylem1  10500  cardidg  10539  ondomon  10554  elwina  10677  elina  10678  wuncval  10733  tskmval  10830  eltskm  10834  recmulnq  10955  elnp  10978  elnpi  10979  npomex  10987  elfzp12  13576  seqp1  13977  hashinf  14291  hashxnn0  14295  hashnn0pnf  14298  hashxrcl  14313  prsshashgt1  14366  hashmap  14391  lsw  14510  ccatfval  14519  ccats1alpha  14565  swrdval  14589  pfxval  14619  splval  14697  splcl  14698  revval  14706  reps  14716  s3sndisj  14910  s3iunsndisj  14911  trclfv  14943  relexp0g  14965  relexpsucnnr  14968  relexp1g  14969  limsupcl  15413  limsupval  15414  clim  15434  rlim  15435  hashbcval  16931  isstruct2  17078  setsvalg  17095  setsfun0  17101  setscom  17109  strfvnd  17114  setsid  17137  ressval  17172  ressinbas  17186  restval  17368  pwsval  17428  xpsfrnel2  17506  ismre  17530  oppcval  17653  oppccatf  17670  brssc  17757  rescval  17770  issubc  17781  isfunc  17810  homadm  17986  homacd  17987  uncfval  18183  pltfval  18280  lubfval  18299  glbfval  18312  joinfval  18322  meetfval  18336  p0val  18376  p1val  18377  oduclatb  18456  ipoval  18479  pws0g  18657  frmdval  18728  vrmdfval  18733  efmnd  18747  efmnd2hash  18771  eqgfval  19050  gaid  19157  cntzfval  19178  elsymgbas  19234  symg2hash  19252  pmtrfval  19311  symggen  19331  gexval  19439  lsmfval  19499  pj1fval  19555  frgpval  19619  vrgpfval  19627  dmdprd  19860  dprdw  19872  pws1  20128  pwsmgp  20130  dvdsr  20165  isrim0OLD  20248  lssset  20532  lspfval  20572  islbs  20675  sraval  20777  zlmval  21049  psgnevpmb  21124  ocvfval  21203  cssval  21219  thlval  21232  dsmmval  21273  dsmmbase  21274  frlmval  21287  uvcfval  21323  islinds  21348  ltbval  21580  evlsval  21631  coe1fval  21711  evls1fval  21820  matval  21893  oftpos  21936  dmatval  21976  scmatval  21988  smadiadetglem2  22156  cpmat  22193  mat2pmatfval  22207  cpm2mfval  22233  decpmatval0  22248  pm2mpval  22279  chpmatfval  22314  basdif0  22438  tgval  22440  eltg  22442  eltg2  22443  neipeltop  22615  ordtval  22675  islocfin  23003  txval  23050  qtopval  23181  isfbas  23315  isfildlem  23343  fmval  23429  fmf  23431  isfcls  23495  alexsubb  23532  tsmsfbas  23614  ustval  23689  elutop  23720  isusp  23748  ispsmet  23792  ismet  23811  isxmet  23812  blfvalps  23871  metustel  24041  tngval  24130  elpi1  24543  rrxval  24886  q1peqb  25654  ig1pval  25672  taylfval  25853  ulmval  25874  elno  27129  nosupno  27186  noetalem2  27225  oldlim  27361  negsval  27480  iscgrg  27743  isismt  27765  legval  27815  ishlg  27833  ishpg  27990  iscgra  28040  isinag  28069  isleag  28078  iseqlg  28098  ttgval  28106  ttgvalOLD  28107  xmstrkgc  28123  cplgr2vpr  28670  vtxdgfval  28704  ewlksfval  28838  wksfval  28846  iswlkg  28850  wwlksnon  29085  wspthsnon  29086  avril1  29696  ispligb  29708  gidval  29743  isvcOLD  29810  0vfval  29837  elunop  31103  rabexgfGS  31717  disjdifprg  31784  disjdifprg2  31785  abfmpunirn  31855  rabfmpunirn  31856  hashgt1  31998  mntoval  32130  tocycval  32245  evpmval  32282  altgnsg  32286  sgnsv  32297  inftmrel  32304  isinftm  32305  resvval  32410  idlsrgval  32569  rprmval  32585  dimval  32632  dimvalfi  32633  smatfval  32713  lmatval  32731  ispcmp  32775  qqhval2  32900  rrhval  32914  xrhval  32936  indv  32948  esumc  32987  esumpad  32991  esumpcvgval  33014  ofcfval3  33038  issiga  33048  baselsiga  33051  sigasspw  33052  issgon  33059  isrnsigau  33063  sigagenval  33076  ispisys2  33089  cldssbrsiga  33123  sxval  33126  ismeas  33135  cnmbfm  33200  mbfmcnt  33205  elcarsg  33242  sitmval  33286  eulerpartlemt0  33306  sseqval  33325  sseqmw  33328  sseqp1  33332  orvcval  33394  orvcval4  33397  ballotlemsv  33446  satf  34282  satfv1lem  34291  satefv  34343  mrexval  34430  mrsubffval  34436  msubffval  34452  mclsval  34492  eldm3  34669  opelco3  34684  elima4  34685  elfix2  34814  elsingles  34828  fvimage  34841  funpartlem  34852  elaltxp  34885  brcolinear2  34968  ellines  35062  topfneec  35178  topfneec2  35179  fnejoin2  35192  limsucncmpi  35268  findabrcl  35277  bj-ififc  35397  elelb  35715  bj-pwvrelb  35716  bj-sngltag  35802  bj-xtagex  35808  bj-elsnb  35880  bj-epelg  35887  bj-evalval  35894  bj-ismoore  35924  bj-ideqg1  35983  bj-ideqg1ALT  35984  bj-elid6  35989  bj-diagval  35993  bj-eldiag2  35996  bj-isrvec  36113  finxpreclem1  36208  finxpreclem3  36212  elghomlem2OLD  36692  isrngo  36703  isdivrngo  36756  br1cnvres  37075  riotasv2d  37765  riotasv3d  37768  lshpset  37786  lsatset  37798  lcvfbr  37828  lflset  37867  lkrfval  37895  lkrval2  37898  islshpkrN  37928  ldualset  37933  cmtfvalN  38018  cvrfval  38076  pats  38093  llnset  38314  lplnset  38338  lvolset  38381  lineset  38547  pointsetN  38550  psubspset  38553  pmapfval  38565  paddfval  38606  pclfvalN  38698  polfvalN  38713  psubclsetN  38745  watfvalN  38801  lhpset  38804  lautset  38891  pautsetN  38907  ldilfset  38917  ltrnfset  38926  dilfsetN  38961  trnfsetN  38964  trlfset  38969  tgrpfset  39553  tendofset  39567  erngfset  39608  erngfset-rN  39616  dvafset  39813  diaffval  39839  dvhfset  39889  docaffvalN  39930  djaffvalN  39942  dibffval  39949  dicffval  39983  dihffval  40039  dochffval  40158  djhffval  40205  lpolsetN  40291  lcdfval  40397  mapdffval  40435  hvmapffval  40567  hdmap1ffval  40604  hdmapffval  40635  hgmapffval  40694  hlhilset  40743  elrab2w  40965  elrfi  41365  nacsfix  41383  mapfzcons2  41390  sbc2rexgOLD  41459  sbc4rexgOLD  41461  setindtrs  41697  wepwso  41718  hbtlem1  41798  hbtlem7  41800  rgspnval  41843  mendval  41858  oaltublim  41973  omord2lim  41983  cnvtrucl0  42308  eliunov2  42363  iunrelexpmin1  42392  iunrelexpmin2  42396  trclfvcom  42407  cnvtrclfv  42408  trclimalb2  42410  trclfvdecomr  42412  gneispacef2  42820  gneispacern2  42823  gneispace0nelrn  42824  addrval  43158  subrval  43159  mulvval  43160  elixpconstg  43711  mptfnd  43879  upbdrech  43950  climf  44273  climf2  44317  liminfval  44410  dvcosre  44563  itgsinexplem1  44605  itgsubsticclem  44626  dmvolss  44636  stoweidlem26  44677  stoweidlem35  44686  stirlinglem14  44738  fourierdlem42  44800  fourierdlem81  44838  fourierdlem89  44846  fourierdlem91  44848  salgenval  44972  elsprel  46078  sprval  46082  prprval  46117  upwlksfval  46448  isupwlkg  46450  intopval  46547  clintopval  46549  assintopval  46550  isrngisom  46628  rngcvalALTV  46761  rnghmsscmap  46774  ringcvalALTV  46807  rhmsscmap  46820  dmatbas  46986  lincop  46991  lcoop  46994  fdivval  47127  blenval  47159  itcoval  47249  itcoval1  47251  itcoval2  47252  itcoval3  47253  itcovalsucov  47256  lines  47319  spheres  47334