Theorem elex 3455

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 1850	. 2 ⊢ (∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐵) → ∃𝑥 𝑥 = 𝐴)
2		dfclel 2864	. 2 ⊢ (𝐴 ∈ 𝐵 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐵))
3		isset 3449	. 2 ⊢ (𝐴 ∈ V ↔ ∃𝑥 𝑥 = 𝐴)
4	1, 2, 3	3imtr4i 293	1 ⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ V)

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1522  ∃wex 1761   ∈ wcel 2081  Vcvv 3437

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-ext 2769

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1762  df-sb 2043  df-clab 2776  df-cleq 2788  df-clel 2863  df-v 3439

This theorem is referenced by:  elexi  3456  elexd  3457  elissetOLD  3458  prcnel  3461  vtoclgf  3508  vtocl2gf  3512  vtocl3gf  3513  vtocl2g  3514  spcimgft  3529  spcimdv  3535  spcgv  3538  spc3egv  3546  elab4g  3609  elrabf  3614  elrab  3618  mob  3644  sbcex  3716  sbcel1v  3767  sbcel1vOLD  3768  sbcabel  3789  csbiebt  3837  eldif  3869  ssv  3912  elun  4046  elin  4090  csbnestgf  4291  sbcco3g  4294  csbco3g  4295  csbvarg  4298  sbccsb2  4301  ifexg  4428  elpwb  4464  elpr2  4496  snidb  4505  ifpr  4536  eldifvsn  4637  prnesn  4697  elpreqpr  4704  dfopg  4708  eluni  4748  eliun  4829  csbexg  5105  nvel  5111  class2seteq  5146  axpweq  5156  reusv2lem4  5193  opeqsng  5284  elopab  5304  epelg  5354  epelgOLD  5355  opelvvg  5483  opeliunxp2  5595  opelres  5740  imasng  5827  elimasni  5832  iniseg  5836  inisegn0  5837  dmmptg  5971  elon2  6077  ordsssuc2  6154  iota2  6215  fnmptf  6352  fnmpt  6356  fvelimab  6605  mpteqb  6653  fvmptt  6654  fvmptf  6655  fvopab5  6665  fvopab6  6666  fprg  6780  eloprabga  7117  ovmpos  7154  ov2gf  7155  ovmpox  7159  ovmpoga  7160  ovmpt3rab1  7261  brrpssg  7309  sorpssi  7313  unexg  7329  elpwun  7348  ordeleqon  7359  onintrab  7372  sucexg  7381  ordsucelsuc  7393  onzsl  7417  elxp5  7484  offval3  7539  releldm2  7598  fnmpo  7623  mpoexg  7630  mptmpoopabbrd  7634  bropfvvvv  7643  suppval  7683  opeliunxp2f  7727  brtpos2  7749  undefval  7793  tfr2b  7884  tz7.49  7932  oeordi  8063  relelec  8184  ecdmn0  8186  mapvalg  8266  pmvalg  8267  elpmg  8272  elixp2  8314  mptelixpg  8347  elixpsn  8349  snmapen  8438  2pwuninel  8519  fival  8722  elfi2  8724  dffi2  8733  elfiun  8740  wemappo  8859  wemapso  8861  wemapso2lem  8862  harval  8872  brwdom  8877  fowdom  8881  brwdom2  8883  brwdom3  8892  en2lp  8915  cantnfsuc  8979  rankvalb  9072  rankwflem  9090  rankr1g  9107  r1pwALT  9121  r1rankid  9134  djulcl  9185  djurcl  9186  inlresf  9189  inrresf  9191  djuss  9195  1stinl  9202  2ndinl  9203  1stinr  9204  2ndinr  9205  cardval3  9227  dfac8alem  9301  isacn  9316  numacn  9321  acndom  9323  cardinfima  9369  unialeph  9373  ackbij1lem5  9492  cflm  9518  isf32lem2  9622  isfin1-2  9653  itunifval  9684  numth3  9738  ttukeylem1  9777  cardidg  9816  ondomon  9831  canth4  9915  canthnumlem  9916  canthwelem  9918  elwina  9954  elina  9955  wuncval  10010  tskmval  10107  eltskm  10111  recmulnq  10232  elnp  10255  elnpi  10256  npomex  10264  elfzp12  12836  seqp1  13234  hashinf  13545  hashxnn0  13549  hashnn0pnf  13552  hashxrcl  13568  prsshashgt1  13619  hashmap  13644  lsw  13762  ccatfval  13771  ccats1alpha  13817  swrdval  13841  pfxval  13871  cats1un  13919  splval  13949  splcl  13950  revval  13958  reps  13968  s3sndisj  14161  s3iunsndisj  14162  trclfv  14194  relexp0g  14215  relexpsucnnr  14218  relexp1g  14219  limsupcl  14664  limsupval  14665  clim  14685  rlim  14686  hashbcval  16167  isstruct2  16322  strfvnd  16331  setsvalg  16341  setsfun0  16348  setscom  16356  setsid  16367  ressval  16380  ressinbas  16389  restval  16529  pwsval  16588  xpsfrnel2  16666  ismre  16690  oppcval  16812  brssc  16913  rescval  16926  issubc  16934  isfunc  16963  homadm  17129  homacd  17130  uncfval  17313  pltfval  17398  pospo  17412  lubfval  17417  glbfval  17430  joinfval  17440  meetfval  17454  p0val  17480  p1val  17481  oduclatb  17583  ipoval  17593  pws0g  17765  frmdval  17827  vrmdfval  17832  eqgfval  18081  gaid  18170  cntzfval  18191  symgval  18238  elsymgbas  18241  symg2hash  18256  pmtrfval  18309  symggen  18329  gexval  18433  lsmfval  18493  pj1fval  18547  frgpval  18611  vrgpfval  18619  dmdprd  18837  dprdw  18849  pws1  19056  pwsmgp  19058  dvdsr  19086  isrim0  19165  lssset  19395  lspfval  19435  islbs  19538  sraval  19638  ltbval  19939  evlsval  19986  evlsval2  19987  coe1fval  20056  evls1fval  20165  zlmval  20345  psgnevpmb  20413  ocvfval  20492  cssval  20508  thlval  20521  dsmmval  20560  dsmmbase  20561  frlmval  20574  uvcfval  20610  islinds  20635  matval  20704  oftpos  20745  dmatval  20785  scmatval  20797  smadiadetglem2  20965  cpmat  21001  mat2pmatfval  21015  cpm2mfval  21041  decpmatval0  21056  pm2mpval  21087  chpmatfval  21122  basdif0  21245  tgval  21247  eltg  21249  eltg2  21250  neipeltop  21421  islp  21432  ordtval  21481  islocfin  21809  txval  21856  qtopval  21987  isfbas  22121  isfildlem  22149  snfil  22156  cfinfil  22185  csdfil  22186  supfil  22187  fin1aufil  22224  fmval  22235  fmf  22237  isfcls  22301  alexsubb  22338  tsmsfbas  22419  ustval  22494  elutop  22525  isusp  22553  ispsmet  22597  ismet  22616  isxmet  22617  blfvalps  22676  metustel  22843  tngval  22931  elpi1  23332  rrxval  23673  q1peqb  24431  ig1pval  24449  taylfval  24630  ulmval  24651  iscgrg  25980  isismt  26002  legval  26052  ishlg  26070  ishpg  26227  iscgra  26277  isinag  26307  isleag  26316  iseqlg  26336  ttgval  26344  xmstrkgc  26355  cplgr2vpr  26898  vtxdgfval  26932  1loopgrnb0  26967  ewlksfval  27066  wksfval  27074  iswlkg  27078  wwlksnon  27316  wspthsnon  27317  avril1  27933  ispligb  27945  gidval  27980  isvcOLD  28047  0vfval  28074  elunop  29340  rabexgfGS  29954  disjdifprg  30015  disjdifprg2  30016  abfmpunirn  30087  rabfmpunirn  30088  fcobijfs  30147  hashgt1  30214  tocycval  30397  evpmval  30424  altgnsg  30429  sgnsv  30440  inftmrel  30447  isinftm  30448  resvval  30554  dimval  30605  dimvalfi  30606  smatfval  30675  lmatval  30693  ispcmp  30738  qqhval2  30840  rrhval  30854  xrhval  30876  indv  30888  esumc  30927  esumpad  30931  esumpcvgval  30954  ofcfval3  30978  issiga  30988  baselsiga  30991  sigasspw  30992  issgon  30999  isrnsigau  31003  sigagenval  31016  ispisys2  31029  cldssbrsiga  31063  sxval  31066  ismeas  31075  cnmbfm  31138  mbfmcnt  31143  omsfval  31169  elcarsg  31180  sitmval  31224  eulerpartlemt0  31244  sseqval  31263  sseqmw  31266  sseqp1  31270  orvcval  31332  orvcval4  31335  ballotlemsv  31384  satf  32208  satfv1lem  32217  satefv  32269  mrexval  32356  mrsubffval  32362  msubffval  32378  mclsval  32418  eldm3  32605  opelco3  32626  elima4  32627  elno  32762  nosupno  32812  noetalem5  32830  nulsslt  32871  nulssgt  32872  elfix2  32974  elsingles  32988  fvimage  33001  funpartlem  33012  elaltxp  33045  brcolinear2  33128  ellines  33222  topfneec  33312  topfneec2  33313  fnejoin2  33326  limsucncmpi  33402  findabrcl  33411  elelb  33785  bj-sngltag  33900  bj-xtagex  33906  bj-epelg  33959  bj-evalval  33964  bj-ismoorec  33997  bj-diagval  34033  bj-eldiag2  34035  finxpreclem1  34201  finxpreclem3  34205  poimirlem17  34440  elghomlem2OLD  34696  isrngo  34707  isdivrngo  34760  cnvepresex  35123  riotasv2d  35624  riotasv3d  35627  lshpset  35645  lsatset  35657  lcvfbr  35687  lflset  35726  lkrfval  35754  lkrval2  35757  islshpkrN  35787  ldualset  35792  cmtfvalN  35877  cvrfval  35935  pats  35952  llnset  36172  lplnset  36196  lvolset  36239  lineset  36405  pointsetN  36408  psubspset  36411  pmapfval  36423  paddfval  36464  pclfvalN  36556  polfvalN  36571  psubclsetN  36603  watfvalN  36659  lhpset  36662  lautset  36749  pautsetN  36765  ldilfset  36775  ltrnfset  36784  dilfsetN  36819  trnfsetN  36822  trlfset  36827  tgrpfset  37411  tendofset  37425  erngfset  37466  erngfset-rN  37474  dvafset  37671  diaffval  37697  dvhfset  37747  docaffvalN  37788  djaffvalN  37800  dibffval  37807  dicffval  37841  dihffval  37897  dochffval  38016  djhffval  38063  lpolsetN  38149  lcdfval  38255  mapdffval  38293  hvmapffval  38425  hdmap1ffval  38462  hdmapffval  38493  hgmapffval  38552  hlhilset  38601  elrfi  38776  nacsfix  38794  mapfzcons2  38801  sbc2rexgOLD  38870  sbc4rexgOLD  38872  setindtrs  39107  wepwso  39128  hbtlem1  39208  hbtlem7  39210  rgspnval  39253  mendval  39268  cnvtrucl0  39469  eliunov2  39509  iunrelexpmin1  39538  iunrelexpmin2  39542  trclfvcom  39553  cnvtrclfv  39554  trclimalb2  39556  trclfvdecomr  39558  gneispacef2  39971  gneispacern2  39974  gneispace0nelrn  39975  addrval  40337  subrval  40338  mulvval  40339  elixpconstg  40894  mptfnd  41053  upbdrech  41113  climf  41445  climf2  41489  liminfval  41582  dvcosre  41737  itgsinexplem1  41780  itgsubsticclem  41801  dmvolss  41812  stoweidlem26  41853  stoweidlem35  41862  stirlinglem14  41914  fourierdlem42  41976  fourierdlem81  42014  fourierdlem89  42022  fourierdlem91  42024  salgenval  42148  elsprel  43119  sprval  43123  prprval  43158  upwlksfval  43492  isupwlkg  43494  intopval  43587  clintopval  43589  assintopval  43590  isrngisom  43645  rngcvalALTV  43710  rnghmsscmap  43723  ringcvalALTV  43756  rhmsscmap  43769  dmatbas  43938  lincop  43943  lcoop  43946  offval0  44045  fdivval  44080  blenval  44112  lines  44199  spheres  44214