Theorem elex 3451

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 3446	. 2 ⊢ (𝐴 ∈ V ↔ ∃𝑥 𝑥 = 𝐴)
4	1, 2, 3	3imtr4i 292	1 ⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ V)

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1539  ∃wex 1782   ∈ wcel 2107  Vcvv 3433

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 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-v 3435

This theorem is referenced by:  elexi  3452  elexd  3453  prcnel  3456  vtoclgf  3504  vtocl2gf  3509  vtocl3gf  3510  vtocl2g  3511  vtocl3g  3512  spcimgft  3527  spcgv  3536  spc3egv  3543  elab4g  3615  elrabf  3621  elrab  3625  mob  3653  sbcex  3727  sbcel1v  3788  sbcabel  3812  csbiebt  3863  eldif  3898  elin  3904  ssv  3946  elun  4084  csbnestgfw  4354  sbcco3gw  4357  csbnestgf  4359  sbcco3g  4362  csbco3g  4363  csbvarg  4366  sbccsb2  4369  elpwb  4544  pwidb  4557  elpr2g  4586  elpr2OLD  4588  snidb  4597  ifpr  4628  eldifvsn  4731  preqsnd  4790  elpreqpr  4798  dfopg  4803  eluni  4843  eliun  4929  csbexg  5235  nvel  5241  class2seteq  5278  axpweq  5288  reusv2lem4  5325  elopab  5441  epelg  5497  opelvvg  5630  opeliunxp2  5750  opelres  5900  imasng  5994  elimasni  6002  iniseg  6008  inisegn0  6009  dmmptg  6150  elon2  6281  ordsssuc2  6358  iota2  6426  fnmptf  6578  fnmpt  6582  fvelimab  6850  mpteqb  6903  fvmptt  6904  fvmptf  6905  fvopab5  6916  fvopab6  6917  fprg  7036  eloprabga  7391  eloprabgaOLD  7392  ovmpos  7430  ov2gf  7431  ovmpox  7435  ovmpoga  7436  ovmpt3rab1  7536  brrpssg  7587  sorpssi  7591  unexg  7608  elpwun  7628  ordeleqon  7641  onintrab  7655  sucexg  7664  ordsucelsuc  7678  onzsl  7702  dmfexALT  7766  elxp5  7779  offval3  7834  releldm2  7893  fnmpo  7918  mpoexg  7926  mptmpoopabbrdOLD  7932  bropfvvvv  7941  fsplitfpar  7968  suppval  7988  opeliunxp2f  8035  brtpos2  8057  undefval  8101  tfr2b  8236  tz7.49  8285  oeordi  8427  relelec  8552  ecdmn0  8554  mapvalg  8634  pmvalg  8635  elpmg  8640  elixp2  8698  mptelixpg  8732  elixpsn  8734  2pwuninel  8928  fival  9180  elfi2  9182  dffi2  9191  elfiun  9198  wemapso2lem  9320  harval  9328  brwdom  9335  fowdom  9339  brwdom2  9341  brwdom3  9350  en2lp  9373  cantnfsuc  9437  rankvalb  9564  rankwflem  9582  rankr1g  9599  r1pwALT  9613  r1rankid  9626  djulcl  9677  djurcl  9678  inlresf  9681  inrresf  9683  djuss  9687  1stinl  9694  2ndinl  9695  1stinr  9696  2ndinr  9697  cardval3  9719  dfac8alem  9794  isacn  9809  numacn  9814  acndom  9816  cardinfima  9862  unialeph  9866  ackbij1lem5  9989  cflm  10015  isf32lem2  10119  isfin1-2  10150  itunifval  10181  numth3  10235  ttukeylem1  10274  cardidg  10313  ondomon  10328  elwina  10451  elina  10452  wuncval  10507  tskmval  10604  eltskm  10608  recmulnq  10729  elnp  10752  elnpi  10753  npomex  10761  elfzp12  13344  seqp1  13745  hashinf  14058  hashxnn0  14062  hashnn0pnf  14065  hashxrcl  14081  prsshashgt1  14134  hashmap  14159  lsw  14276  ccatfval  14285  ccats1alpha  14333  swrdval  14365  pfxval  14395  splval  14473  splcl  14474  revval  14482  reps  14492  s3sndisj  14687  s3iunsndisj  14688  trclfv  14720  relexp0g  14742  relexpsucnnr  14745  relexp1g  14746  limsupcl  15191  limsupval  15192  clim  15212  rlim  15213  hashbcval  16712  isstruct2  16859  setsvalg  16876  setsfun0  16882  setscom  16890  strfvnd  16895  setsid  16918  ressval  16953  ressinbas  16964  restval  17146  pwsval  17206  xpsfrnel2  17284  ismre  17308  oppcval  17431  oppccatf  17448  brssc  17535  rescval  17548  issubc  17559  isfunc  17588  homadm  17764  homacd  17765  uncfval  17961  pltfval  18058  lubfval  18077  glbfval  18090  joinfval  18100  meetfval  18114  p0val  18154  p1val  18155  oduclatb  18234  ipoval  18257  pws0g  18430  frmdval  18499  vrmdfval  18504  efmnd  18518  efmnd2hash  18542  eqgfval  18813  gaid  18914  cntzfval  18935  elsymgbas  18990  symg2hash  19008  pmtrfval  19067  symggen  19087  gexval  19192  lsmfval  19252  pj1fval  19309  frgpval  19373  vrgpfval  19381  dmdprd  19610  dprdw  19622  pws1  19864  pwsmgp  19866  dvdsr  19897  isrim0  19976  lssset  20204  lspfval  20244  islbs  20347  sraval  20447  zlmval  20726  psgnevpmb  20801  ocvfval  20880  cssval  20896  thlval  20909  dsmmval  20950  dsmmbase  20951  frlmval  20964  uvcfval  21000  islinds  21025  ltbval  21253  evlsval  21305  coe1fval  21385  evls1fval  21494  matval  21567  oftpos  21610  dmatval  21650  scmatval  21662  smadiadetglem2  21830  cpmat  21867  mat2pmatfval  21881  cpm2mfval  21907  decpmatval0  21922  pm2mpval  21953  chpmatfval  21988  basdif0  22112  tgval  22114  eltg  22116  eltg2  22117  neipeltop  22289  ordtval  22349  islocfin  22677  txval  22724  qtopval  22855  isfbas  22989  isfildlem  23017  fmval  23103  fmf  23105  isfcls  23169  alexsubb  23206  tsmsfbas  23288  ustval  23363  elutop  23394  isusp  23422  ispsmet  23466  ismet  23485  isxmet  23486  blfvalps  23545  metustel  23715  tngval  23804  elpi1  24217  rrxval  24560  q1peqb  25328  ig1pval  25346  taylfval  25527  ulmval  25548  iscgrg  26882  isismt  26904  legval  26954  ishlg  26972  ishpg  27129  iscgra  27179  isinag  27208  isleag  27217  iseqlg  27237  ttgval  27245  ttgvalOLD  27246  xmstrkgc  27262  cplgr2vpr  27809  vtxdgfval  27843  ewlksfval  27977  wksfval  27985  iswlkg  27989  wwlksnon  28225  wspthsnon  28226  avril1  28836  ispligb  28848  gidval  28883  isvcOLD  28950  0vfval  28977  elunop  30243  rabexgfGS  30855  disjdifprg  30923  disjdifprg2  30924  abfmpunirn  30998  rabfmpunirn  30999  hashgt1  31137  mntoval  31269  tocycval  31384  evpmval  31421  altgnsg  31425  sgnsv  31436  inftmrel  31443  isinftm  31444  resvval  31535  idlsrgval  31657  rprmval  31673  dimval  31695  dimvalfi  31696  smatfval  31754  lmatval  31772  ispcmp  31816  qqhval2  31941  rrhval  31955  xrhval  31977  indv  31989  esumc  32028  esumpad  32032  esumpcvgval  32055  ofcfval3  32079  issiga  32089  baselsiga  32092  sigasspw  32093  issgon  32100  isrnsigau  32104  sigagenval  32117  ispisys2  32130  cldssbrsiga  32164  sxval  32167  ismeas  32176  cnmbfm  32239  mbfmcnt  32244  elcarsg  32281  sitmval  32325  eulerpartlemt0  32345  sseqval  32364  sseqmw  32367  sseqp1  32371  orvcval  32433  orvcval4  32436  ballotlemsv  32485  satf  33324  satfv1lem  33333  satefv  33385  mrexval  33472  mrsubffval  33478  msubffval  33494  mclsval  33534  eldm3  33737  opelco3  33758  elima4  33759  elno  33858  nosupno  33915  noetalem2  33954  oldlim  34078  negsval  34132  elfix2  34215  elsingles  34229  fvimage  34242  funpartlem  34253  elaltxp  34286  brcolinear2  34369  ellines  34463  topfneec  34553  topfneec2  34554  fnejoin2  34567  limsucncmpi  34643  findabrcl  34652  bj-ififc  34772  elelb  35091  bj-pwvrelb  35092  bj-sngltag  35182  bj-xtagex  35188  bj-elsnb  35241  bj-epelg  35248  bj-evalval  35255  bj-ismoore  35285  bj-ideqg1  35344  bj-ideqg1ALT  35345  bj-elid6  35350  bj-diagval  35354  bj-eldiag2  35357  bj-isrvec  35474  finxpreclem1  35569  finxpreclem3  35573  elghomlem2OLD  36053  isrngo  36064  isdivrngo  36117  riotasv2d  36978  riotasv3d  36981  lshpset  36999  lsatset  37011  lcvfbr  37041  lflset  37080  lkrfval  37108  lkrval2  37111  islshpkrN  37141  ldualset  37146  cmtfvalN  37231  cvrfval  37289  pats  37306  llnset  37526  lplnset  37550  lvolset  37593  lineset  37759  pointsetN  37762  psubspset  37765  pmapfval  37777  paddfval  37818  pclfvalN  37910  polfvalN  37925  psubclsetN  37957  watfvalN  38013  lhpset  38016  lautset  38103  pautsetN  38119  ldilfset  38129  ltrnfset  38138  dilfsetN  38173  trnfsetN  38176  trlfset  38181  tgrpfset  38765  tendofset  38779  erngfset  38820  erngfset-rN  38828  dvafset  39025  diaffval  39051  dvhfset  39101  docaffvalN  39142  djaffvalN  39154  dibffval  39161  dicffval  39195  dihffval  39251  dochffval  39370  djhffval  39417  lpolsetN  39503  lcdfval  39609  mapdffval  39647  hvmapffval  39779  hdmap1ffval  39816  hdmapffval  39847  hgmapffval  39906  hlhilset  39955  elrab2w  40174  elrfi  40523  nacsfix  40541  mapfzcons2  40548  sbc2rexgOLD  40617  sbc4rexgOLD  40619  setindtrs  40854  wepwso  40875  hbtlem1  40955  hbtlem7  40957  rgspnval  41000  mendval  41015  cnvtrucl0  41239  eliunov2  41294  iunrelexpmin1  41323  iunrelexpmin2  41327  trclfvcom  41338  cnvtrclfv  41339  trclimalb2  41341  trclfvdecomr  41343  gneispacef2  41753  gneispacern2  41756  gneispace0nelrn  41757  addrval  42091  subrval  42092  mulvval  42093  elixpconstg  42646  mptfnd  42793  upbdrech  42851  climf  43170  climf2  43214  liminfval  43307  dvcosre  43460  itgsinexplem1  43502  itgsubsticclem  43523  dmvolss  43533  stoweidlem26  43574  stoweidlem35  43583  stirlinglem14  43635  fourierdlem42  43697  fourierdlem81  43735  fourierdlem89  43743  fourierdlem91  43745  salgenval  43869  elsprel  44938  sprval  44942  prprval  44977  upwlksfval  45308  isupwlkg  45310  intopval  45407  clintopval  45409  assintopval  45410  isrngisom  45465  rngcvalALTV  45530  rnghmsscmap  45543  ringcvalALTV  45576  rhmsscmap  45589  dmatbas  45755  lincop  45760  lcoop  45763  fdivval  45896  blenval  45928  itcoval  46018  itcoval1  46020  itcoval2  46021  itcoval3  46022  itcovalsucov  46025  lines  46088  spheres  46103