Theorem elex 3485

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1533  ∃wex 1773   ∈ wcel 2098  Vcvv 3466

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2695

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1536  df-ex 1774  df-sb 2060  df-clab 2702  df-cleq 2716  df-clel 2802  df-v 3468

This theorem is referenced by:  elexi  3486  elexd  3487  prcnel  3490  vtoclgft  3533  vtoclgf  3550  vtocl2gf  3553  vtocl3gf  3554  vtocl2g  3555  vtocl3g  3556  spcimgft  3569  spcgv  3578  spc3egv  3585  elab4g  3666  elrabf  3672  elrab  3676  class2seteq  3693  mob  3706  sbcex  3780  sbcel1v  3841  sbcabel  3865  csbiebt  3916  eldif  3951  elin  3957  ssv  3999  elun  4141  csbnestgfw  4412  sbcco3gw  4415  csbnestgf  4417  sbcco3g  4420  csbco3g  4421  csbvarg  4424  sbccsb2  4427  elpwb  4603  pwidb  4616  elpr2g  4645  elpr2OLD  4647  snidb  4656  ifpr  4688  snssg  4780  eldifvsn  4793  preqsnd  4852  elpreqpr  4860  dfopg  4864  eluni  4903  eliun  4992  csbexg  5301  nvel  5307  axpweq  5339  reusv2lem4  5390  elopab  5518  epelg  5572  opelvvg  5708  opeliunxp2  5829  opelres  5978  imasng  6073  elimasni  6081  iniseg  6087  inisegn0  6088  dmmptg  6232  elon2  6366  ordsssuc2  6446  iota2  6523  fnmptf  6677  fnmpt  6681  fvelimab  6955  mpteqb  7008  fvmptt  7009  fvmptf  7010  fvopab5  7021  fvopab6  7022  fprg  7146  eloprabga  7509  eloprabgaOLD  7510  ovmpos  7549  ov2gf  7550  ovmpox  7554  ovmpoga  7555  ovmpt3rab1  7658  brrpssg  7709  sorpssi  7713  unexg  7730  elpwun  7750  ordeleqon  7763  onintrab  7778  sucexg  7787  sucexeloni  7791  ordsucelsuc  7804  onzsl  7829  dmfexALT  7895  elxp5  7908  offval3  7963  releldm2  8023  fnmpo  8049  mpoexg  8057  mptmpoopabbrdOLDOLD  8064  bropfvvvv  8073  fsplitfpar  8099  suppval  8143  opeliunxp2f  8191  brtpos2  8213  undefval  8257  tfr2b  8392  tz7.49  8441  oeordi  8583  relelec  8745  ecdmn0  8747  mapvalg  8827  pmvalg  8828  elpmg  8834  elixp2  8892  mptelixpg  8926  elixpsn  8928  2pwuninel  9129  rex2dom  9243  fival  9404  elfi2  9406  dffi2  9415  elfiun  9422  wemapso2lem  9544  harval  9552  brwdom  9559  fowdom  9563  brwdom2  9565  brwdom3  9574  en2lp  9598  cantnfsuc  9662  rankvalb  9789  rankwflem  9807  rankr1g  9824  r1pwALT  9838  r1rankid  9851  djulcl  9902  djurcl  9903  inlresf  9906  inrresf  9908  djuss  9912  1stinl  9919  2ndinl  9920  1stinr  9921  2ndinr  9922  cardval3  9944  dfac8alem  10021  isacn  10036  numacn  10041  acndom  10043  cardinfima  10089  unialeph  10093  ackbij1lem5  10216  cflm  10242  isf32lem2  10346  isfin1-2  10377  itunifval  10408  numth3  10462  ttukeylem1  10501  cardidg  10540  ondomon  10555  elwina  10678  elina  10679  wuncval  10734  tskmval  10831  eltskm  10835  recmulnq  10956  elnp  10979  elnpi  10980  npomex  10988  elfzp12  13578  seqp1  13979  hashinf  14293  hashxnn0  14297  hashnn0pnf  14300  hashxrcl  14315  prsshashgt1  14368  hashmap  14393  lsw  14512  ccatfval  14521  ccats1alpha  14567  swrdval  14591  pfxval  14621  splval  14699  splcl  14700  revval  14708  reps  14718  s3sndisj  14912  s3iunsndisj  14913  trclfv  14945  relexp0g  14967  relexpsucnnr  14970  relexp1g  14971  limsupcl  15415  limsupval  15416  clim  15436  rlim  15437  hashbcval  16936  isstruct2  17083  setsvalg  17100  setsfun0  17106  setscom  17114  strfvnd  17119  setsid  17142  ressval  17177  ressinbas  17191  restval  17373  pwsval  17433  xpsfrnel2  17511  ismre  17535  oppcval  17658  oppccatf  17675  brssc  17762  rescval  17775  issubc  17786  isfunc  17815  homadm  17994  homacd  17995  uncfval  18191  pltfval  18288  lubfval  18307  glbfval  18320  joinfval  18330  meetfval  18344  p0val  18384  p1val  18385  oduclatb  18464  ipoval  18487  pws0g  18695  frmdval  18768  vrmdfval  18773  efmnd  18787  efmnd2hash  18811  eqgfval  19095  gaid  19207  cntzfval  19228  elsymgbas  19285  symg2hash  19303  pmtrfval  19362  symggen  19382  gexval  19490  lsmfval  19550  pj1fval  19606  frgpval  19670  vrgpfval  19678  dmdprd  19912  dprdw  19924  pws1  20216  pwsmgp  20218  dvdsr  20256  isrngim  20339  isrim0OLD  20375  rnghmsscmap  20518  rhmsscmap  20547  lssset  20772  lspfval  20812  islbs  20916  sraval  21015  zlmval  21372  psgnevpmb  21450  ocvfval  21529  cssval  21545  thlval  21558  dsmmval  21599  dsmmbase  21600  frlmval  21613  uvcfval  21649  islinds  21674  ltbval  21910  evlsval  21961  coe1fval  22049  evls1fval  22162  matval  22235  oftpos  22278  dmatval  22318  scmatval  22330  smadiadetglem2  22498  cpmat  22535  mat2pmatfval  22549  cpm2mfval  22575  decpmatval0  22590  pm2mpval  22621  chpmatfval  22656  basdif0  22780  tgval  22782  eltg  22784  eltg2  22785  neipeltop  22957  ordtval  23017  islocfin  23345  txval  23392  qtopval  23523  isfbas  23657  isfildlem  23685  fmval  23771  fmf  23773  isfcls  23837  alexsubb  23874  tsmsfbas  23956  ustval  24031  elutop  24062  isusp  24090  ispsmet  24134  ismet  24153  isxmet  24154  blfvalps  24213  metustel  24383  tngval  24472  elpi1  24896  rrxval  25239  q1peqb  26014  ig1pval  26032  taylfval  26214  ulmval  26235  elno  27498  nosupno  27555  noetalem2  27594  oldlim  27732  negsval  27857  iscgrg  28235  isismt  28257  legval  28307  ishlg  28325  ishpg  28482  iscgra  28532  isinag  28561  isleag  28570  iseqlg  28590  ttgval  28598  ttgvalOLD  28599  xmstrkgc  28615  cplgr2vpr  29162  vtxdgfval  29196  ewlksfval  29330  wksfval  29338  iswlkg  29342  wwlksnon  29577  wspthsnon  29578  avril1  30188  ispligb  30202  gidval  30237  isvcOLD  30304  0vfval  30331  elunop  31597  rabexgfGS  32211  disjdifprg  32278  disjdifprg2  32279  abfmpunirn  32349  rabfmpunirn  32350  hashgt1  32492  mntoval  32622  tocycval  32738  evpmval  32775  altgnsg  32779  sgnsv  32790  inftmrel  32797  isinftm  32798  resvval  32910  idlsrgval  33089  rprmval  33105  dimval  33167  dimvalfi  33168  smatfval  33267  lmatval  33285  ispcmp  33329  qqhval2  33454  rrhval  33468  xrhval  33490  indv  33502  esumc  33541  esumpad  33545  esumpcvgval  33568  ofcfval3  33592  issiga  33602  baselsiga  33605  sigasspw  33606  issgon  33613  isrnsigau  33617  sigagenval  33630  ispisys2  33643  cldssbrsiga  33677  sxval  33680  ismeas  33689  cnmbfm  33754  mbfmcnt  33759  elcarsg  33796  sitmval  33840  eulerpartlemt0  33860  sseqval  33879  sseqmw  33882  sseqp1  33886  orvcval  33948  orvcval4  33951  ballotlemsv  34000  satf  34835  satfv1lem  34844  satefv  34896  mrexval  34983  mrsubffval  34989  msubffval  35005  mclsval  35045  eldm3  35227  opelco3  35242  elima4  35243  elfix2  35372  elsingles  35386  fvimage  35399  funpartlem  35410  elaltxp  35443  brcolinear2  35526  ellines  35620  topfneec  35731  topfneec2  35732  fnejoin2  35745  limsucncmpi  35821  findabrcl  35830  bj-ififc  35950  elelb  36268  bj-pwvrelb  36269  bj-sngltag  36355  bj-xtagex  36361  bj-elsnb  36433  bj-epelg  36440  bj-evalval  36447  bj-ismoore  36477  bj-ideqg1  36536  bj-ideqg1ALT  36537  bj-elid6  36542  bj-diagval  36546  bj-eldiag2  36549  bj-isrvec  36666  finxpreclem1  36761  finxpreclem3  36765  elghomlem2OLD  37248  isrngo  37259  isdivrngo  37312  br1cnvres  37631  riotasv2d  38321  riotasv3d  38324  lshpset  38342  lsatset  38354  lcvfbr  38384  lflset  38423  lkrfval  38451  lkrval2  38454  islshpkrN  38484  ldualset  38489  cmtfvalN  38574  cvrfval  38632  pats  38649  llnset  38870  lplnset  38894  lvolset  38937  lineset  39103  pointsetN  39106  psubspset  39109  pmapfval  39121  paddfval  39162  pclfvalN  39254  polfvalN  39269  psubclsetN  39301  watfvalN  39357  lhpset  39360  lautset  39447  pautsetN  39463  ldilfset  39473  ltrnfset  39482  dilfsetN  39517  trnfsetN  39520  trlfset  39525  tgrpfset  40109  tendofset  40123  erngfset  40164  erngfset-rN  40172  dvafset  40369  diaffval  40395  dvhfset  40445  docaffvalN  40486  djaffvalN  40498  dibffval  40505  dicffval  40539  dihffval  40595  dochffval  40714  djhffval  40761  lpolsetN  40847  lcdfval  40953  mapdffval  40991  hvmapffval  41123  hdmap1ffval  41160  hdmapffval  41191  hgmapffval  41250  hlhilset  41299  elrab2w  41924  elrfi  41946  nacsfix  41964  mapfzcons2  41971  sbc2rexgOLD  42040  sbc4rexgOLD  42042  setindtrs  42278  wepwso  42299  hbtlem1  42379  hbtlem7  42381  rgspnval  42424  mendval  42439  oaltublim  42554  omord2lim  42564  cnvtrucl0  42889  eliunov2  42944  iunrelexpmin1  42973  iunrelexpmin2  42977  trclfvcom  42988  cnvtrclfv  42989  trclimalb2  42991  trclfvdecomr  42993  gneispacef2  43401  gneispacern2  43404  gneispace0nelrn  43405  addrval  43739  subrval  43740  mulvval  43741  elixpconstg  44291  mptfnd  44455  upbdrech  44525  climf  44848  climf2  44892  liminfval  44985  dvcosre  45138  itgsinexplem1  45180  itgsubsticclem  45201  dmvolss  45211  stoweidlem26  45252  stoweidlem35  45261  stirlinglem14  45313  fourierdlem42  45375  fourierdlem81  45413  fourierdlem89  45421  fourierdlem91  45423  salgenval  45547  elsprel  46653  sprval  46657  prprval  46692  upwlksfval  47023  isupwlkg  47025  intopval  47090  clintopval  47092  assintopval  47093  rngcvalALTV  47153  ringcvalALTV  47177  dmatbas  47297  lincop  47302  lcoop  47305  fdivval  47438  blenval  47470  itcoval  47560  itcoval1  47562  itcoval2  47563  itcoval3  47564  itcovalsucov  47567  lines  47630  spheres  47645