Theorem elex 3440

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 2818	. 2 ⊢ (𝐴 ∈ 𝐵 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐵))
3		isset 3435	. 2 ⊢ (𝐴 ∈ V ↔ ∃𝑥 𝑥 = 𝐴)
4	1, 2, 3	3imtr4i 291	1 ⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ V)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1539  ∃wex 1783   ∈ wcel 2108  Vcvv 3422

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424

This theorem is referenced by:  elexi  3441  elexd  3442  prcnel  3445  vtoclgf  3493  vtocl2gf  3498  vtocl3gf  3499  vtocl2g  3500  vtocl3g  3501  spcimgft  3516  spcgv  3525  spc3egv  3532  elab4g  3607  elrabf  3613  elrab  3617  mob  3647  sbcex  3721  sbcel1v  3783  sbcabel  3807  csbiebt  3858  eldif  3893  elin  3899  ssv  3941  elun  4079  csbnestgfw  4350  sbcco3gw  4353  csbnestgf  4355  sbcco3g  4358  csbco3g  4359  csbvarg  4362  sbccsb2  4365  elpwb  4540  pwidb  4553  elpr2g  4582  elpr2OLD  4584  snidb  4593  ifpr  4624  eldifvsn  4727  preqsnd  4786  elpreqpr  4794  dfopg  4799  eluni  4839  eliun  4925  csbexg  5229  nvel  5235  class2seteq  5272  axpweq  5282  reusv2lem4  5319  elopab  5433  epelg  5487  opelvvg  5620  opeliunxp2  5736  opelres  5886  imasng  5980  elimasni  5988  iniseg  5994  inisegn0  5995  dmmptg  6134  elon2  6262  ordsssuc2  6339  iota2  6407  fnmptf  6553  fnmpt  6557  fvelimab  6823  mpteqb  6876  fvmptt  6877  fvmptf  6878  fvopab5  6889  fvopab6  6890  fprg  7009  eloprabga  7360  eloprabgaOLD  7361  ovmpos  7399  ov2gf  7400  ovmpox  7404  ovmpoga  7405  ovmpt3rab1  7505  brrpssg  7556  sorpssi  7560  unexg  7577  elpwun  7597  ordeleqon  7609  onintrab  7623  sucexg  7632  ordsucelsuc  7644  onzsl  7668  dmfexALT  7731  elxp5  7744  offval3  7798  releldm2  7857  fnmpo  7882  mpoexg  7890  mptmpoopabbrd  7894  bropfvvvv  7903  fsplitfpar  7930  suppval  7950  opeliunxp2f  7997  brtpos2  8019  undefval  8063  tfr2b  8198  tz7.49  8246  oeordi  8380  relelec  8501  ecdmn0  8503  mapvalg  8583  pmvalg  8584  elpmg  8589  elixp2  8647  mptelixpg  8681  elixpsn  8683  2pwuninel  8868  fival  9101  elfi2  9103  dffi2  9112  elfiun  9119  wemapso2lem  9241  harval  9249  brwdom  9256  fowdom  9260  brwdom2  9262  brwdom3  9271  en2lp  9294  cantnfsuc  9358  rankvalb  9486  rankwflem  9504  rankr1g  9521  r1pwALT  9535  r1rankid  9548  djulcl  9599  djurcl  9600  inlresf  9603  inrresf  9605  djuss  9609  1stinl  9616  2ndinl  9617  1stinr  9618  2ndinr  9619  cardval3  9641  dfac8alem  9716  isacn  9731  numacn  9736  acndom  9738  cardinfima  9784  unialeph  9788  ackbij1lem5  9911  cflm  9937  isf32lem2  10041  isfin1-2  10072  itunifval  10103  numth3  10157  ttukeylem1  10196  cardidg  10235  ondomon  10250  elwina  10373  elina  10374  wuncval  10429  tskmval  10526  eltskm  10530  recmulnq  10651  elnp  10674  elnpi  10675  npomex  10683  elfzp12  13264  seqp1  13664  hashinf  13977  hashxnn0  13981  hashnn0pnf  13984  hashxrcl  14000  prsshashgt1  14053  hashmap  14078  lsw  14195  ccatfval  14204  ccats1alpha  14252  swrdval  14284  pfxval  14314  splval  14392  splcl  14393  revval  14401  reps  14411  s3sndisj  14606  s3iunsndisj  14607  trclfv  14639  relexp0g  14661  relexpsucnnr  14664  relexp1g  14665  limsupcl  15110  limsupval  15111  clim  15131  rlim  15132  hashbcval  16631  isstruct2  16778  setsvalg  16795  setsfun0  16801  setscom  16809  strfvnd  16814  setsid  16837  ressval  16870  ressinbas  16881  restval  17054  pwsval  17114  xpsfrnel2  17192  ismre  17216  oppcval  17339  oppccatf  17356  brssc  17443  rescval  17456  issubc  17466  isfunc  17495  homadm  17671  homacd  17672  uncfval  17868  pltfval  17964  lubfval  17983  glbfval  17996  joinfval  18006  meetfval  18020  p0val  18060  p1val  18061  oduclatb  18140  ipoval  18163  pws0g  18336  frmdval  18405  vrmdfval  18410  efmnd  18424  efmnd2hash  18448  eqgfval  18719  gaid  18820  cntzfval  18841  elsymgbas  18896  symg2hash  18914  pmtrfval  18973  symggen  18993  gexval  19098  lsmfval  19158  pj1fval  19215  frgpval  19279  vrgpfval  19287  dmdprd  19516  dprdw  19528  pws1  19770  pwsmgp  19772  dvdsr  19803  isrim0  19882  lssset  20110  lspfval  20150  islbs  20253  sraval  20353  zlmval  20629  psgnevpmb  20704  ocvfval  20783  cssval  20799  thlval  20812  dsmmval  20851  dsmmbase  20852  frlmval  20865  uvcfval  20901  islinds  20926  ltbval  21154  evlsval  21206  coe1fval  21286  evls1fval  21395  matval  21468  oftpos  21509  dmatval  21549  scmatval  21561  smadiadetglem2  21729  cpmat  21766  mat2pmatfval  21780  cpm2mfval  21806  decpmatval0  21821  pm2mpval  21852  chpmatfval  21887  basdif0  22011  tgval  22013  eltg  22015  eltg2  22016  neipeltop  22188  ordtval  22248  islocfin  22576  txval  22623  qtopval  22754  isfbas  22888  isfildlem  22916  fmval  23002  fmf  23004  isfcls  23068  alexsubb  23105  tsmsfbas  23187  ustval  23262  elutop  23293  isusp  23321  ispsmet  23365  ismet  23384  isxmet  23385  blfvalps  23444  metustel  23612  tngval  23701  elpi1  24114  rrxval  24456  q1peqb  25224  ig1pval  25242  taylfval  25423  ulmval  25444  iscgrg  26777  isismt  26799  legval  26849  ishlg  26867  ishpg  27024  iscgra  27074  isinag  27103  isleag  27112  iseqlg  27132  ttgval  27140  xmstrkgc  27156  cplgr2vpr  27703  vtxdgfval  27737  ewlksfval  27871  wksfval  27879  iswlkg  27883  wwlksnon  28117  wspthsnon  28118  avril1  28728  ispligb  28740  gidval  28775  isvcOLD  28842  0vfval  28869  elunop  30135  rabexgfGS  30747  disjdifprg  30815  disjdifprg2  30816  abfmpunirn  30891  rabfmpunirn  30892  hashgt1  31030  mntoval  31162  tocycval  31277  evpmval  31314  altgnsg  31318  sgnsv  31329  inftmrel  31336  isinftm  31337  resvval  31428  idlsrgval  31550  rprmval  31566  dimval  31588  dimvalfi  31589  smatfval  31647  lmatval  31665  ispcmp  31709  qqhval2  31832  rrhval  31846  xrhval  31868  indv  31880  esumc  31919  esumpad  31923  esumpcvgval  31946  ofcfval3  31970  issiga  31980  baselsiga  31983  sigasspw  31984  issgon  31991  isrnsigau  31995  sigagenval  32008  ispisys2  32021  cldssbrsiga  32055  sxval  32058  ismeas  32067  cnmbfm  32130  mbfmcnt  32135  elcarsg  32172  sitmval  32216  eulerpartlemt0  32236  sseqval  32255  sseqmw  32258  sseqp1  32262  orvcval  32324  orvcval4  32327  ballotlemsv  32376  satf  33215  satfv1lem  33224  satefv  33276  mrexval  33363  mrsubffval  33369  msubffval  33385  mclsval  33425  eldm3  33634  opelco3  33655  elima4  33656  elno  33776  nosupno  33833  noetalem2  33872  oldlim  33996  negsval  34050  elfix2  34133  elsingles  34147  fvimage  34160  funpartlem  34171  elaltxp  34204  brcolinear2  34287  ellines  34381  topfneec  34471  topfneec2  34472  fnejoin2  34485  limsucncmpi  34561  findabrcl  34570  bj-ififc  34690  elelb  35009  bj-pwvrelb  35010  bj-sngltag  35100  bj-xtagex  35106  bj-elsnb  35159  bj-epelg  35166  bj-evalval  35173  bj-ismoore  35203  bj-ideqg1  35262  bj-ideqg1ALT  35263  bj-elid6  35268  bj-diagval  35272  bj-eldiag2  35275  bj-isrvec  35392  finxpreclem1  35487  finxpreclem3  35491  elghomlem2OLD  35971  isrngo  35982  isdivrngo  36035  riotasv2d  36898  riotasv3d  36901  lshpset  36919  lsatset  36931  lcvfbr  36961  lflset  37000  lkrfval  37028  lkrval2  37031  islshpkrN  37061  ldualset  37066  cmtfvalN  37151  cvrfval  37209  pats  37226  llnset  37446  lplnset  37470  lvolset  37513  lineset  37679  pointsetN  37682  psubspset  37685  pmapfval  37697  paddfval  37738  pclfvalN  37830  polfvalN  37845  psubclsetN  37877  watfvalN  37933  lhpset  37936  lautset  38023  pautsetN  38039  ldilfset  38049  ltrnfset  38058  dilfsetN  38093  trnfsetN  38096  trlfset  38101  tgrpfset  38685  tendofset  38699  erngfset  38740  erngfset-rN  38748  dvafset  38945  diaffval  38971  dvhfset  39021  docaffvalN  39062  djaffvalN  39074  dibffval  39081  dicffval  39115  dihffval  39171  dochffval  39290  djhffval  39337  lpolsetN  39423  lcdfval  39529  mapdffval  39567  hvmapffval  39699  hdmap1ffval  39736  hdmapffval  39767  hgmapffval  39826  hlhilset  39875  elrab2w  40095  elrfi  40432  nacsfix  40450  mapfzcons2  40457  sbc2rexgOLD  40526  sbc4rexgOLD  40528  setindtrs  40763  wepwso  40784  hbtlem1  40864  hbtlem7  40866  rgspnval  40909  mendval  40924  cnvtrucl0  41121  eliunov2  41176  iunrelexpmin1  41205  iunrelexpmin2  41209  trclfvcom  41220  cnvtrclfv  41221  trclimalb2  41223  trclfvdecomr  41225  gneispacef2  41635  gneispacern2  41638  gneispace0nelrn  41639  addrval  41973  subrval  41974  mulvval  41975  elixpconstg  42528  mptfnd  42675  upbdrech  42734  climf  43053  climf2  43097  liminfval  43190  dvcosre  43343  itgsinexplem1  43385  itgsubsticclem  43406  dmvolss  43416  stoweidlem26  43457  stoweidlem35  43466  stirlinglem14  43518  fourierdlem42  43580  fourierdlem81  43618  fourierdlem89  43626  fourierdlem91  43628  salgenval  43752  elsprel  44815  sprval  44819  prprval  44854  upwlksfval  45185  isupwlkg  45187  intopval  45284  clintopval  45286  assintopval  45287  isrngisom  45342  rngcvalALTV  45407  rnghmsscmap  45420  ringcvalALTV  45453  rhmsscmap  45466  dmatbas  45632  lincop  45637  lcoop  45640  fdivval  45773  blenval  45805  itcoval  45895  itcoval1  45897  itcoval2  45898  itcoval3  45899  itcovalsucov  45902  lines  45965  spheres  45980