Theorem elex 3212

Description: If a class is a member of another class, 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 1795	. 2 ⊢ (∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐵) → ∃𝑥 𝑥 = 𝐴)
2		df-clel 2618	. 2 ⊢ (𝐴 ∈ 𝐵 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐵))
3		isset 3207	. 2 ⊢ (𝐴 ∈ V ↔ ∃𝑥 𝑥 = 𝐴)
4	1, 2, 3	3imtr4i 281	1 ⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ V)

Syntax hints:   → wi 4   ∧ wa 384   = wceq 1483  ∃wex 1704   ∈ wcel 1990  Vcvv 3200

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-12 2047  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-an 386  df-tru 1486  df-ex 1705  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-v 3202

This theorem is referenced by:  elexi  3213  elexd  3214  elisset  3215  prcnel  3218  vtoclgftOLD  3255  vtoclgf  3264  vtoclg1f  3265  vtocl2gf  3268  vtocl3gf  3269  spcimgft  3284  elab4g  3355  elrabf  3360  mob  3388  sbcex  3445  sbcel1v  3495  sbcabel  3517  csbiebt  3553  eldif  3584  ssv  3625  elun  3753  elin  3796  csbnestgf  3996  sbcco3g  3999  csbco3g  4000  csbvarg  4003  sbccsb2  4005  elpwb  4169  elpr2  4199  snidb  4207  ifpr  4233  eldifvsn  4326  elpreqpr  4396  dfopg  4400  eluni  4439  eliun  4524  csbexg  4792  nvel  4797  class2seteq  4833  axpweq  4842  reusv2lem4  4872  elopab  4983  epelg  5030  opelvvg  5165  opeliunxp2  5260  imasng  5487  elimasni  5492  iniseg  5496  inisegn0  5497  dmmptg  5632  elon2  5734  ordsssuc2  5814  iota2  5877  fnmptf  6016  fnmpt  6020  dmmptd  6024  elfvex  6221  fvelimab  6253  fvmptdv2  6298  mpteqb  6299  fvmptt  6300  fvmptf  6301  fvopab5  6309  fvopab6  6310  fprg  6422  fmptpr  6438  tpres  6466  eloprabga  6747  ovmpt2s  6784  ov2gf  6785  ovmpt2dxf  6786  ovmpt2x  6789  ovmpt2ga  6790  ovmpt2df  6792  ovmpt3rab1  6891  brrpssg  6939  sorpssi  6943  unexg  6959  elpwun  6977  ordeleqon  6988  onintrab  7001  sucexg  7010  ordsucelsuc  7022  onzsl  7046  elxp5  7111  offval3  7162  releldm2  7218  fnmpt2  7238  mpt2exg  7245  mptmpt2opabbrd  7248  offval22  7253  bropfvvvv  7257  suppval  7297  mptsuppd  7318  suppssov1  7327  suppssfv  7331  opeliunxp2f  7336  brtpos2  7358  undefval  7402  tfr2b  7492  tz7.49  7540  oeordi  7667  oeeu  7683  relelec  7787  ecdmn0  7789  mapvalg  7867  pmvalg  7868  elpmg  7873  elixp2  7912  mptelixpg  7945  elixpsn  7947  2pwuninel  8115  fival  8318  elfi2  8320  dffi2  8329  elfiun  8336  wemappo  8454  wemapso  8456  wemapso2lem  8457  harval  8467  brwdom  8472  fowdom  8476  brwdom2  8478  brwdom3  8487  en2lp  8510  cantnfsuc  8567  cnfcomlem  8596  rankvalb  8660  rankwflem  8678  rankr1g  8695  r1pwALT  8709  r1rankid  8722  cardval3  8778  pm54.43lem  8825  dfac8alem  8852  ac5num  8859  isacn  8867  numacn  8872  acndom  8874  cardinfima  8920  unialeph  8924  cdaval  8992  cflm  9072  isf32lem2  9176  isfin1-2  9207  itunifval  9238  numth3  9292  ttukeylem1  9331  ttukeylem3  9333  cardidg  9370  ondomon  9385  canth4  9469  canthnumlem  9470  canthwelem  9472  elwina  9508  elina  9509  wuncval  9564  grothpw  9648  tskmval  9661  eltskm  9665  recmulnq  9786  elnp  9809  elnpi  9810  npomex  9818  elfzp12  12419  mptnn0fsupp  12797  mptnn0fsuppr  12799  seqp1  12816  seqf1olem2  12841  hashinf  13122  hashxnn0  13127  hashnn0pnf  13130  hashxrcl  13148  prsshashgt1  13198  hashbclem  13236  lsw  13351  ccatfval  13358  swrdval  13417  cats1un  13475  splval  13502  splcl  13503  revval  13509  reps  13517  s3sndisj  13706  s3iunsndisj  13707  trclfv  13741  relexp0g  13762  relexpsucnnr  13765  relexp1g  13766  limsupcl  14204  limsupval  14205  clim  14225  rlim  14226  fsumrlim  14543  hashbcval  15706  isstruct2  15867  strfvnd  15876  setsvalg  15887  setsfun0  15894  setscom  15903  strfv2d  15905  setsid  15914  ressval  15927  ressinbas  15936  restval  16087  prdsval  16115  prdssca  16116  pwsval  16146  imasval  16171  qusval  16202  xpsfrnel  16223  xpsfrnel2  16225  xpsval  16232  ismre  16250  oppcval  16373  brssc  16474  rescval  16487  issubc  16495  isfunc  16524  cofuval  16542  resfval  16552  funcres2c  16561  homadm  16690  homacd  16691  setcval  16727  catcval  16746  estrcval  16764  estrres  16779  xpcval  16817  prfval  16839  curfval  16863  uncfval  16874  pltfval  16959  pospo  16973  lubfval  16978  glbfval  16991  joinfval  17001  meetfval  17015  p0val  17041  p1val  17042  oduclatb  17144  ipoval  17154  ipodrsima  17165  prdsmndd  17323  prds0g  17324  pws0g  17326  frmdval  17388  vrmdfval  17393  prdsgrpd  17525  prdsinvgd  17526  eqgfval  17642  eqgval  17643  gaid  17732  cntzfval  17753  symgval  17799  elsymgbas  17802  symg2hash  17817  pmtrfval  17870  symggen  17890  gexval  17993  lsmfval  18053  pj1fval  18107  frgpval  18171  vrgpfval  18179  prdscmnd  18264  dmdprd  18397  dprdw  18409  pws1  18616  pwsmgp  18618  dvdsr  18646  isirred  18699  isrim0  18723  issrng  18850  lssset  18934  prdslmodd  18969  lspfval  18973  islbs  19076  sraval  19176  psrval  19362  mvrfval  19420  ltbval  19471  opsrval  19474  evlsval  19519  evlsval2  19520  coe1fval  19575  evls1fval  19684  zlmval  19864  psgnevpmb  19933  ocvfval  20010  cssval  20026  thlval  20039  dsmmval  20078  dsmmbase  20079  frlmval  20092  uvcfval  20123  elfilspd  20142  islinds  20148  mamufval  20191  matval  20217  oftpos  20258  dmatval  20298  scmatval  20310  mvmulfval  20348  smadiadetglem2  20478  cpmat  20514  mat2pmatfval  20528  cpm2mfval  20554  decpmatval0  20569  pm2mpval  20600  chpmatfval  20635  basdif0  20757  tgval  20759  eltg  20761  eltg2  20762  neipeltop  20933  islp  20944  ordtval  20993  dis2ndc  21263  islocfin  21320  txval  21367  qtopval  21498  elmptrab2OLD  21631  elmptrab2  21632  isfbas  21633  isfildlem  21661  snfil  21668  cfinfil  21697  csdfil  21698  supfil  21699  fin1aufil  21736  fmval  21747  fmf  21749  isfcls  21813  alexsub  21849  alexsubb  21850  tsmsfbas  21931  tsmsval2  21933  ustval  22006  elutop  22037  isusp  22065  ispsmet  22109  ismet  22128  isxmet  22129  prdsdsf  22172  prdsxmet  22174  blfvalps  22188  metustel  22355  tngval  22443  elpi1  22845  rrxval  23175  itgfsum  23593  q1peqb  23914  ig1pval  23932  taylfval  24113  ulmval  24134  mtest  24158  iscgrg  25407  isismt  25429  legval  25479  ishlg  25497  mirval  25550  perpln1  25605  perpln2  25606  isperp  25607  ishpg  25651  midf  25668  ismidb  25670  lmif  25677  islmib  25679  iscgra  25701  isinag  25729  isleag  25733  iseqlg  25747  f1otrg  25751  f1otrge  25752  ttgval  25755  xmstrkgc  25766  vtxvalOLD  25880  iedgvalOLD  25881  edgvalOLD  25942  uvtxaval  26287  cplgr2vpr  26329  vtxdgfval  26363  1loopgrnb0  26398  ewlksfval  26497  wksfval  26505  iswlkg  26509  wwlksnon  26738  wspthsnon  26739  wlknwwlksnsur  26776  avril1  27319  ispligb  27329  gidval  27366  isvcOLD  27434  0vfval  27461  elunop  28731  rabexgfGS  29340  disjdifprg  29388  disjdifprg2  29389  abfmpunirn  29452  rabfmpunirn  29453  funcnvmptOLD  29467  funcnvmpt  29468  fcobijfs  29501  sgnsv  29727  inftmrel  29734  isinftm  29735  resvval  29827  smatfval  29861  lmatval  29879  ispcmp  29924  qqhval2  30026  rrhval  30040  xrhval  30062  indv  30074  esumc  30113  esumpad  30117  esumpcvgval  30140  ofcfval  30160  ofcfval3  30164  issiga  30174  baselsiga  30178  sigasspw  30179  issgon  30186  isrnsigau  30190  sigagenval  30203  ispisys2  30216  cldssbrsiga  30250  sxval  30253  ismeas  30262  cnmbfm  30325  mbfmcnt  30330  omsfval  30356  elcarsg  30367  sitmval  30411  eulerpartlemt0  30431  sseqval  30450  sseqmw  30453  sseqp1  30457  orvcval  30519  orvcval4  30522  ballotlemsv  30571  mrexval  31398  mrsubffval  31404  msubffval  31420  mclsval  31460  eldm3  31651  opelco3  31678  elima4  31679  wsuclemOLD  31774  elno  31799  nosupno  31849  noetalem5  31867  nulsslt  31908  nulssgt  31909  elfix2  32011  elsingles  32025  fvimage  32038  funpartlem  32049  elaltxp  32082  brcolinear2  32165  ellines  32259  topfneec  32350  topfneec2  32351  fnejoin2  32364  limsucncmpi  32444  findabrcl  32453  bj-sngltag  32971  bj-xtagex  32977  bj-evalval  33027  bj-ismoorec  33060  bj-diagval  33090  bj-eldiag2  33092  finxpreclem1  33226  finxpreclem3  33230  poimirlem17  33426  opelopab3  33511  elghomlem2OLD  33685  isrngo  33696  isdivrngo  33749  opelresALTV  34031  cnvepresex  34104  riotasv2d  34243  riotasv3d  34246  lshpset  34265  lsatset  34277  lcvfbr  34307  lflset  34346  lkrfval  34374  lkrval2  34377  islshpkrN  34407  ldualset  34412  cmtfvalN  34497  cvrfval  34555  pats  34572  llnset  34791  lplnset  34815  lvolset  34858  lineset  35024  pointsetN  35027  psubspset  35030  pmapfval  35042  paddfval  35083  pclfvalN  35175  polfvalN  35190  psubclsetN  35222  watfvalN  35278  lhpset  35281  lautset  35368  pautsetN  35384  ldilfset  35394  ltrnfset  35403  dilfsetN  35439  trnfsetN  35442  trlfset  35447  tgrpfset  36032  tendofset  36046  erngfset  36087  erngfset-rN  36095  dvafset  36292  diaffval  36319  dvhfset  36369  docaffvalN  36410  djaffvalN  36422  dibffval  36429  dicffval  36463  dihffval  36519  dochffval  36638  djhffval  36685  lpolsetN  36771  lcdfval  36877  mapdffval  36915  hvmapffval  37047  hdmap1ffval  37085  hdmapffval  37118  hgmapffval  37177  hlhilset  37226  elrfi  37257  nacsfix  37275  mapfzcons2  37282  sbc2rexgOLD  37352  sbc4rexgOLD  37354  setindtrs  37592  wepwso  37613  hbtlem1  37693  hbtlem7  37695  rgspnval  37738  mendval  37753  cnvtrucl0  37931  eliunov2  37971  iunrelexpmin1  38000  iunrelexpmin2  38004  trclfvcom  38015  cnvtrclfv  38016  trclimalb2  38018  trclfvdecomr  38020  frege81d  38039  frege129d  38055  gneispacef2  38434  gneispacern2  38437  gneispace0nelrn  38438  addrval  38670  subrval  38671  mulvval  38672  elixpconstg  39266  dmmptdf  39417  dmmptdf2  39439  mptfnd  39451  upbdrech  39519  climf  39854  climf2  39898  liminfval  39991  dvcosre  40126  itgsinexplem1  40169  itgsubsticclem  40191  dmvolss  40202  stoweidlem26  40243  stoweidlem35  40252  stirlinglem14  40304  fourierdlem42  40366  fourierdlem81  40404  fourierdlem89  40412  fourierdlem91  40414  salgenval  40541  ismea  40668  pfxval  41383  upwlksfval  41716  isupwlkg  41718  elsprel  41725  sprval  41729  intopval  41838  clintopval  41840  assintopval  41841  isrngisom  41896  rngcvalALTV  41961  rngcval  41962  rnghmsscmap  41974  ringcvalALTV  42007  ringcval  42008  rhmsscmap  42020  dmatbas  42192  lincop  42197  lcoop  42200  offval0  42299  fdivval  42333  blenval  42365