Theorem elex 3512

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 1869	. 2 ⊢ (∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐵) → ∃𝑥 𝑥 = 𝐴)
2		dfclel 2894	. 2 ⊢ (𝐴 ∈ 𝐵 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐵))
3		isset 3506	. 2 ⊢ (𝐴 ∈ V ↔ ∃𝑥 𝑥 = 𝐴)
4	1, 2, 3	3imtr4i 294	1 ⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ V)

Syntax hints:   → wi 4   ∧ wa 398   = wceq 1537  ∃wex 1780   ∈ wcel 2114  Vcvv 3494

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-v 3496

This theorem is referenced by:  elexi  3513  elexd  3514  elissetOLD  3515  prcnel  3518  vtoclgf  3565  vtocl2gf  3570  vtocl3gf  3571  vtocl2g  3572  spcimgft  3586  spcgv  3595  spc3egv  3604  elab4g  3671  elrabf  3676  elrab  3680  mob  3708  sbcex  3782  sbcel1v  3839  sbcel1vOLD  3840  sbcabel  3861  csbiebt  3912  eldif  3946  ssv  3991  elun  4125  elin  4169  csbnestgfw  4371  sbcco3gw  4374  csbnestgf  4376  sbcco3g  4379  csbco3g  4380  csbvarg  4383  sbccsb2  4386  ifexg  4514  elpwb  4549  pwidb  4562  elpr2  4591  snidb  4600  ifpr  4629  eldifvsn  4730  prnesn  4790  elpreqpr  4797  dfopg  4801  eluni  4841  eliun  4923  csbexg  5214  nvel  5220  class2seteq  5255  axpweq  5265  reusv2lem4  5302  opeqsng  5393  elopab  5414  epelg  5466  epelgOLD  5467  opelvvg  5595  opeliunxp2  5709  opelres  5859  imasng  5951  elimasni  5956  iniseg  5960  inisegn0  5961  dmmptg  6096  elon2  6202  ordsssuc2  6279  iota2  6344  fnmptf  6484  fnmpt  6488  fvelimab  6737  mpteqb  6787  fvmptt  6788  fvmptf  6789  fvopab5  6800  fvopab6  6801  fprg  6917  eloprabga  7261  ovmpos  7298  ov2gf  7299  ovmpox  7303  ovmpoga  7304  ovmpt3rab1  7403  brrpssg  7451  sorpssi  7455  unexg  7472  elpwun  7491  ordeleqon  7503  onintrab  7516  sucexg  7525  ordsucelsuc  7537  onzsl  7561  elxp5  7628  offval3  7683  releldm2  7742  fnmpo  7767  mpoexg  7774  mptmpoopabbrd  7778  bropfvvvv  7787  fsplitfpar  7814  suppval  7832  opeliunxp2f  7876  brtpos2  7898  undefval  7942  tfr2b  8032  tz7.49  8081  oeordi  8213  relelec  8334  ecdmn0  8336  mapvalg  8416  pmvalg  8417  elpmg  8422  elixp2  8465  mptelixpg  8499  elixpsn  8501  snmapen  8590  2pwuninel  8672  fival  8876  elfi2  8878  dffi2  8887  elfiun  8894  wemappo  9013  wemapso  9015  wemapso2lem  9016  harval  9026  brwdom  9031  fowdom  9035  brwdom2  9037  brwdom3  9046  en2lp  9069  cantnfsuc  9133  rankvalb  9226  rankwflem  9244  rankr1g  9261  r1pwALT  9275  r1rankid  9288  djulcl  9339  djurcl  9340  inlresf  9343  inrresf  9345  djuss  9349  1stinl  9356  2ndinl  9357  1stinr  9358  2ndinr  9359  cardval3  9381  dfac8alem  9455  isacn  9470  numacn  9475  acndom  9477  cardinfima  9523  unialeph  9527  ackbij1lem5  9646  cflm  9672  isf32lem2  9776  isfin1-2  9807  itunifval  9838  numth3  9892  ttukeylem1  9931  cardidg  9970  ondomon  9985  canth4  10069  canthnumlem  10070  canthwelem  10072  elwina  10108  elina  10109  wuncval  10164  tskmval  10261  eltskm  10265  recmulnq  10386  elnp  10409  elnpi  10410  npomex  10418  elfzp12  12987  seqp1  13385  hashinf  13696  hashxnn0  13700  hashnn0pnf  13703  hashxrcl  13719  prsshashgt1  13772  hashmap  13797  lsw  13916  ccatfval  13925  ccats1alpha  13973  swrdval  14005  pfxval  14035  splval  14113  splcl  14114  revval  14122  reps  14132  s3sndisj  14327  s3iunsndisj  14328  trclfv  14360  relexp0g  14381  relexpsucnnr  14384  relexp1g  14385  limsupcl  14830  limsupval  14831  clim  14851  rlim  14852  hashbcval  16338  isstruct2  16493  strfvnd  16502  setsvalg  16512  setsfun0  16519  setscom  16527  setsid  16538  ressval  16551  ressinbas  16560  restval  16700  pwsval  16759  xpsfrnel2  16837  ismre  16861  oppcval  16983  brssc  17084  rescval  17097  issubc  17105  isfunc  17134  homadm  17300  homacd  17301  uncfval  17484  pltfval  17569  pospo  17583  lubfval  17588  glbfval  17601  joinfval  17611  meetfval  17625  p0val  17651  p1val  17652  oduclatb  17754  ipoval  17764  pws0g  17947  frmdval  18016  vrmdfval  18021  efmnd  18035  efmnd2hash  18059  eqgfval  18328  gaid  18429  cntzfval  18450  elsymgbas  18502  symg2hash  18520  pmtrfval  18578  symggen  18598  gexval  18703  lsmfval  18763  pj1fval  18820  frgpval  18884  vrgpfval  18892  dmdprd  19120  dprdw  19132  pws1  19366  pwsmgp  19368  dvdsr  19396  isrim0  19475  lssset  19705  lspfval  19745  islbs  19848  sraval  19948  ltbval  20252  evlsval  20299  evlsval2  20300  coe1fval  20373  evls1fval  20482  zlmval  20663  psgnevpmb  20731  ocvfval  20810  cssval  20826  thlval  20839  dsmmval  20878  dsmmbase  20879  frlmval  20892  uvcfval  20928  islinds  20953  matval  21020  oftpos  21061  dmatval  21101  scmatval  21113  smadiadetglem2  21281  cpmat  21317  mat2pmatfval  21331  cpm2mfval  21357  decpmatval0  21372  pm2mpval  21403  chpmatfval  21438  basdif0  21561  tgval  21563  eltg  21565  eltg2  21566  neipeltop  21737  islp  21748  ordtval  21797  islocfin  22125  txval  22172  qtopval  22303  isfbas  22437  isfildlem  22465  snfil  22472  cfinfil  22501  csdfil  22502  supfil  22503  fin1aufil  22540  fmval  22551  fmf  22553  isfcls  22617  alexsubb  22654  tsmsfbas  22736  ustval  22811  elutop  22842  isusp  22870  ispsmet  22914  ismet  22933  isxmet  22934  blfvalps  22993  metustel  23160  tngval  23248  elpi1  23649  rrxval  23990  q1peqb  24748  ig1pval  24766  taylfval  24947  ulmval  24968  iscgrg  26298  isismt  26320  legval  26370  ishlg  26388  ishpg  26545  iscgra  26595  isinag  26624  isleag  26633  iseqlg  26653  ttgval  26661  xmstrkgc  26672  cplgr2vpr  27215  vtxdgfval  27249  1loopgrnb0  27284  ewlksfval  27383  wksfval  27391  iswlkg  27395  wwlksnon  27629  wspthsnon  27630  avril1  28242  ispligb  28254  gidval  28289  isvcOLD  28356  0vfval  28383  elunop  29649  rabexgfGS  30262  disjdifprg  30325  disjdifprg2  30326  abfmpunirn  30397  rabfmpunirn  30398  fcobijfs  30459  hashgt1  30530  tocycval  30750  evpmval  30787  altgnsg  30791  sgnsv  30802  inftmrel  30809  isinftm  30810  resvval  30900  dimval  31001  dimvalfi  31002  smatfval  31060  lmatval  31078  ispcmp  31121  qqhval2  31223  rrhval  31237  xrhval  31259  indv  31271  esumc  31310  esumpad  31314  esumpcvgval  31337  ofcfval3  31361  issiga  31371  baselsiga  31374  sigasspw  31375  issgon  31382  isrnsigau  31386  sigagenval  31399  ispisys2  31412  cldssbrsiga  31446  sxval  31449  ismeas  31458  cnmbfm  31521  mbfmcnt  31526  elcarsg  31563  sitmval  31607  eulerpartlemt0  31627  sseqval  31646  sseqmw  31649  sseqp1  31653  orvcval  31715  orvcval4  31718  ballotlemsv  31767  satf  32600  satfv1lem  32609  satefv  32661  mrexval  32748  mrsubffval  32754  msubffval  32770  mclsval  32810  eldm3  32997  opelco3  33018  elima4  33019  elno  33153  nosupno  33203  noetalem5  33221  nulsslt  33262  nulssgt  33263  elfix2  33365  elsingles  33379  fvimage  33392  funpartlem  33403  elaltxp  33436  brcolinear2  33519  ellines  33613  topfneec  33703  topfneec2  33704  fnejoin2  33717  limsucncmpi  33793  findabrcl  33802  bj-ififc  33915  elelb  34216  bj-pwvrelb  34217  bj-sngltag  34298  bj-xtagex  34304  bj-elsnb  34357  bj-epelg  34363  bj-evalval  34369  bj-ismoore  34400  bj-ideqg1  34459  bj-ideqg1ALT  34460  bj-elid6  34465  bj-diagval  34469  bj-eldiag2  34472  finxpreclem1  34673  finxpreclem3  34677  poimirlem17  34924  elghomlem2OLD  35179  isrngo  35190  isdivrngo  35243  cnvepresex  35606  riotasv2d  36108  riotasv3d  36111  lshpset  36129  lsatset  36141  lcvfbr  36171  lflset  36210  lkrfval  36238  lkrval2  36241  islshpkrN  36271  ldualset  36276  cmtfvalN  36361  cvrfval  36419  pats  36436  llnset  36656  lplnset  36680  lvolset  36723  lineset  36889  pointsetN  36892  psubspset  36895  pmapfval  36907  paddfval  36948  pclfvalN  37040  polfvalN  37055  psubclsetN  37087  watfvalN  37143  lhpset  37146  lautset  37233  pautsetN  37249  ldilfset  37259  ltrnfset  37268  dilfsetN  37303  trnfsetN  37306  trlfset  37311  tgrpfset  37895  tendofset  37909  erngfset  37950  erngfset-rN  37958  dvafset  38155  diaffval  38181  dvhfset  38231  docaffvalN  38272  djaffvalN  38284  dibffval  38291  dicffval  38325  dihffval  38381  dochffval  38500  djhffval  38547  lpolsetN  38633  lcdfval  38739  mapdffval  38777  hvmapffval  38909  hdmap1ffval  38946  hdmapffval  38977  hgmapffval  39036  hlhilset  39085  elrfi  39311  nacsfix  39329  mapfzcons2  39336  sbc2rexgOLD  39405  sbc4rexgOLD  39407  setindtrs  39642  wepwso  39663  hbtlem1  39743  hbtlem7  39745  rgspnval  39788  mendval  39803  cnvtrucl0  40004  eliunov2  40044  iunrelexpmin1  40073  iunrelexpmin2  40077  trclfvcom  40088  cnvtrclfv  40089  trclimalb2  40091  trclfvdecomr  40093  gneispacef2  40506  gneispacern2  40509  gneispace0nelrn  40510  addrval  40818  subrval  40819  mulvval  40820  elixpconstg  41375  mptfnd  41532  upbdrech  41592  climf  41923  climf2  41967  liminfval  42060  dvcosre  42216  itgsinexplem1  42259  itgsubsticclem  42280  dmvolss  42290  stoweidlem26  42331  stoweidlem35  42340  stirlinglem14  42392  fourierdlem42  42454  fourierdlem81  42492  fourierdlem89  42500  fourierdlem91  42502  salgenval  42626  elsprel  43657  sprval  43661  prprval  43696  upwlksfval  44030  isupwlkg  44032  intopval  44129  clintopval  44131  assintopval  44132  isrngisom  44187  rngcvalALTV  44252  rnghmsscmap  44265  ringcvalALTV  44298  rhmsscmap  44311  dmatbas  44478  lincop  44483  lcoop  44486  fdivval  44619  blenval  44651  lines  44738  spheres  44753