MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  elex Structured version   Visualization version   GIF version

Theorem elex 3185
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.
StepHypRef Expression
1 exsimpl 1783 . 2 (∃𝑥(𝑥 = 𝐴𝑥𝐵) → ∃𝑥 𝑥 = 𝐴)
2 df-clel 2606 . 2 (𝐴𝐵 ↔ ∃𝑥(𝑥 = 𝐴𝑥𝐵))
3 isset 3180 . 2 (𝐴 ∈ V ↔ ∃𝑥 𝑥 = 𝐴)
41, 2, 33imtr4i 280 1 (𝐴𝐵𝐴 ∈ V)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383   = wceq 1475  wex 1695  wcel 1977  Vcvv 3173
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-12 2034  ax-ext 2590
This theorem depends on definitions:  df-bi 196  df-an 385  df-tru 1478  df-ex 1696  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-v 3175
This theorem is referenced by:  elexi  3186  elexd  3187  elisset  3188  prcnel  3191  vtoclgftOLD  3228  vtoclgf  3237  vtoclg1f  3238  vtocl2gf  3241  vtocl3gf  3242  spcimgft  3257  elab4g  3324  elrabf  3329  mob  3355  sbcex  3412  sbcel1v  3462  sbcabel  3483  csbiebt  3519  eldif  3550  ssv  3588  elun  3715  elin  3758  csbnestgf  3948  sbcco3g  3951  csbco3g  3952  csbvarg  3955  sbccsb2  3957  elpr2  4147  snidb  4154  ifpr  4180  eldifvsn  4267  elpreqpr  4334  dfopg  4338  eluni  4375  eliun  4460  csbexg  4720  nvel  4725  class2seteq  4759  axpweq  4768  reusv2lem4  4798  elopab  4908  epelg  4950  opelvvg  5087  opeliunxp2  5182  imasng  5406  elimasni  5411  iniseg  5415  inisegn0  5416  dmmptg  5549  elon2  5651  ordsssuc2  5731  iota2  5794  fnmptf  5929  fnmpt  5933  dmmptd  5937  elfvex  6131  fvelimab  6163  fvmptdv2  6206  mpteqb  6207  fvmptt  6208  fvmptf  6209  fvopab5  6217  fvopab6  6218  fprg  6327  fmptpr  6343  tpres  6371  eloprabga  6645  ovmpt2s  6682  ov2gf  6683  ovmpt2dxf  6684  ovmpt2x  6687  ovmpt2ga  6688  ovmpt2df  6690  ovmpt3rab1  6789  brrpssg  6837  sorpssi  6841  unexg  6857  elpwun  6869  ordeleqon  6880  ssonprc  6884  onintrab  6893  sucexg  6902  ordsucelsuc  6914  onzsl  6938  elxp5  7004  offval3  7053  releldm2  7109  fnmpt2  7127  mpt2exg  7134  offval22  7140  bropfvvvv  7144  suppval  7184  mptsuppd  7205  suppssov1  7214  suppssfv  7218  opeliunxp2f  7223  brtpos2  7245  pwuninel  7288  undefval  7289  tfr2b  7379  tz7.49  7427  oeordi  7554  oeeu  7570  relelec  7674  ecdmn0  7676  mapvalg  7754  pmvalg  7755  elpmg  7759  elixp2  7798  mptelixpg  7831  elixpsn  7833  2pwuninel  8000  pwfi  8144  fival  8201  elfi2  8203  dffi2  8212  elfiun  8219  wemappo  8337  wemapso  8339  wemapso2lem  8340  harval  8350  brwdom  8355  fowdom  8359  brwdom2  8361  brwdom3  8370  en2lp  8393  cantnfsuc  8450  cnfcomlem  8479  rankvalb  8543  pwwf  8553  rankwflem  8561  rankr1g  8578  r1pw  8591  r1pwALT  8592  r1rankid  8605  cardval3  8661  pm54.43lem  8708  dfac8alem  8735  ac5num  8742  isacn  8750  numacn  8755  acndom  8757  cardinfima  8803  unialeph  8807  cdaval  8875  cflm  8955  isfin3  9001  isf32lem2  9059  isfin1-2  9090  itunifval  9121  numth3  9175  ttukeylem1  9214  ttukeylem3  9216  cardidg  9249  ondomon  9264  canth4  9348  canthnumlem  9349  canthwelem  9351  elwina  9387  elina  9388  wuncval  9443  grothpw  9527  tskmval  9540  eltskm  9544  recmulnq  9665  elnp  9688  elnpi  9689  npomex  9697  lbinf  10855  elfzp12  12288  mptnn0fsupp  12659  mptnn0fsuppr  12661  seqp1  12678  seqf1olem2  12703  hashinf  12984  hashxnn0  12989  hashnn0pnf  12992  hashxrcl  13010  prsshashgt1  13059  hashbclem  13093  lsw  13204  ccatfval  13211  swrdval  13269  cats1un  13327  splval  13353  splcl  13354  revval  13360  reps  13368  s3sndisj  13554  s3iunsndisj  13555  trclfv  13589  relexp0g  13610  relexpsucnnr  13613  relexp1g  13614  limsupcl  14052  limsupval  14053  clim  14073  rlim  14074  fsumrlim  14384  hashbcval  15544  isstruct2  15704  strfvnd  15710  setsvalg  15719  setsfun0  15726  setscom  15731  strfv2d  15733  setsid  15742  ressval  15754  ressinbas  15763  restval  15910  prdsval  15938  prdssca  15939  pwsval  15969  imasval  15994  qusval  16025  xpsfrnel  16046  xpsfrnel2  16048  xpsval  16055  ismre  16073  oppcval  16196  brssc  16297  rescval  16310  issubc  16318  isfunc  16347  cofuval  16365  resfval  16375  funcres2c  16384  homadm  16513  homacd  16514  setcval  16550  catcval  16569  estrcval  16587  estrres  16602  xpcval  16640  prfval  16662  curfval  16686  uncfval  16697  pltfval  16782  pospo  16796  lubfval  16801  glbfval  16814  joinfval  16824  meetfval  16838  p0val  16864  p1val  16865  pospropd  16957  oduclatb  16967  ipoval  16977  ipodrsima  16988  prdsmndd  17146  prds0g  17147  pws0g  17149  frmdval  17211  vrmdfval  17216  prdsgrpd  17348  prdsinvgd  17349  eqgfval  17465  eqgval  17466  gaid  17555  cntzfval  17576  symgval  17622  elsymgbas  17625  symg2hash  17640  pmtrfval  17693  symggen  17713  gexval  17816  lsmfval  17876  pj1fval  17930  frgpval  17994  vrgpfval  18002  prdscmnd  18087  dmdprd  18220  dprdw  18232  pws1  18439  pwsmgp  18441  dvdsr  18469  isirred  18522  isrim0  18546  issrng  18673  lssset  18755  prdslmodd  18790  lspfval  18794  islbs  18897  sraval  18997  psrval  19183  mvrfval  19241  ltbval  19292  opsrval  19295  evlsval  19340  evlsval2  19341  coe1fval  19396  evls1fval  19505  zlmval  19683  psgnevpmb  19752  ocvfval  19829  cssval  19845  thlval  19858  dsmmval  19897  dsmmbase  19898  frlmval  19911  uvcfval  19942  elfilspd  19961  islinds  19967  mamufval  20010  matval  20036  oftpos  20077  dmatval  20117  scmatval  20129  mvmulfval  20167  smadiadetglem2  20297  cpmat  20333  mat2pmatfval  20347  cpm2mfval  20373  decpmatval0  20388  pm2mpval  20419  chpmatfval  20454  basdif0  20568  tgval  20570  eltg  20572  eltg2  20573  neipeltop  20743  islp  20754  ordtval  20803  dis2ndc  21073  islocfin  21130  txval  21177  qtopval  21308  elmptrab2OLD  21441  elmptrab2  21442  isfbas  21443  isfildlem  21471  snfil  21478  cfinfil  21507  csdfil  21508  supfil  21509  numufl  21529  fin1aufil  21546  fmval  21557  fmf  21559  isfcls  21623  alexsub  21659  alexsubb  21660  tsmsfbas  21741  tsmsval2  21743  ustval  21816  elutop  21847  isusp  21875  ispsmet  21919  ismet  21938  isxmet  21939  prdsdsf  21982  prdsxmet  21984  blfvalps  21998  metustel  22165  tngval  22253  elpi1  22653  rrxval  22983  itgfsum  23399  q1peqb  23718  ig1pval  23736  taylfval  23917  ulmval  23938  mtest  23962  iscgrg  25207  isismt  25229  legval  25279  ishlg  25297  mirval  25350  perpln1  25405  perpln2  25406  isperp  25407  ishpg  25451  midf  25468  ismidb  25470  lmif  25477  islmib  25479  iscgra  25501  isinag  25529  isleag  25533  iseqlg  25547  f1otrg  25551  f1otrge  25552  ttgval  25555  xmstrkgc  25566  vtxval  25677  iedgval  25678  edgaval  25794  edgval  25868  cusgrafilem1  26007  isuvtx  26016  wlks  26047  wlkon  26061  trls  26066  trlon  26070  2trllemA  26080  pths  26096  spths  26097  pthon  26105  spthon  26112  2wlklem1  26127  crcts  26150  cycls  26151  wwlk  26209  wwlkn  26210  wlknwwlknsur  26240  clwlk  26281  clwwlk  26294  clwwlkn  26295  is2wlkonot  26390  is2spthonot  26391  2wlksot  26394  2spthsot  26395  vdgrfval  26422  avril1  26711  gidval  26750  isvcOLD  26818  0vfval  26845  elunop  28115  rabexgfGS  28725  disjdifprg  28770  disjdifprg2  28771  abfmpunirn  28832  rabfmpunirn  28833  funcnvmptOLD  28850  funcnvmpt  28851  fcobijfs  28889  sgnsv  29058  inftmrel  29065  isinftm  29066  resvval  29158  smatfval  29189  lmatval  29207  ispcmp  29252  qqhval2  29354  rrhval  29368  xrhval  29390  indv  29402  esumc  29440  esumpad  29444  esumpcvgval  29467  ofcfval  29487  ofcfval3  29491  issiga  29501  baselsiga  29505  sigasspw  29506  issgon  29513  isrnsigau  29517  sigagenval  29530  ispisys2  29543  cldssbrsiga  29577  sxval  29580  ismeas  29589  cnmbfm  29652  mbfmcnt  29657  omsfval  29683  elcarsg  29694  sitmval  29738  eulerpartlemt0  29758  sseqval  29777  sseqmw  29780  sseqp1  29784  orvcval  29846  orvcval4  29849  ballotlemsv  29898  bnj1463  30377  mrexval  30652  mrsubffval  30658  msubffval  30674  mclsval  30714  eldm3  30905  opelco3  30923  elima4  30924  wsuclemOLD  31018  elno  31043  nobndlem8  31098  nobndup  31099  nobnddown  31100  elfix2  31181  elsingles  31195  fvimage  31208  funpartlem  31219  elaltxp  31252  brcolinear2  31335  ellines  31429  topfneec  31520  topfneec2  31521  fnejoin2  31534  limsucncmpi  31614  findabrcl  31623  bj-sngltag  32164  bj-xtagex  32170  bj-restv  32229  bj-elpw3  32237  bj-diagval  32267  bj-eldiag2  32269  finxpreclem1  32402  finxpreclem3  32406  poimirlem17  32596  opelopab3  32681  elghomlem2OLD  32855  isrngo  32866  isdivrngo  32919  riotasv2d  33261  riotasv3d  33264  lshpset  33283  lsatset  33295  lcvfbr  33325  lflset  33364  lkrfval  33392  lkrval2  33395  islshpkrN  33425  ldualset  33430  cmtfvalN  33515  cvrfval  33573  pats  33590  llnset  33809  lplnset  33833  lvolset  33876  lineset  34042  pointsetN  34045  psubspset  34048  pmapfval  34060  paddfval  34101  pclfvalN  34193  polfvalN  34208  psubclsetN  34240  watfvalN  34296  lhpset  34299  lautset  34386  pautsetN  34402  ldilfset  34412  ltrnfset  34421  dilfsetN  34457  trnfsetN  34460  trlfset  34465  tgrpfset  35050  tendofset  35064  erngfset  35105  erngfset-rN  35113  dvafset  35310  diaffval  35337  dvhfset  35387  docaffvalN  35428  djaffvalN  35440  dibffval  35447  dicffval  35481  dihffval  35537  dochffval  35656  djhffval  35703  lpolsetN  35789  lcdfval  35895  mapdffval  35933  hvmapffval  36065  hdmap1ffval  36103  hdmapffval  36136  hgmapffval  36195  hlhilset  36244  elrfi  36275  nacsfix  36293  mapfzcons2  36300  sbc2rexgOLD  36370  sbc4rexgOLD  36372  setindtrs  36610  wepwso  36631  hbtlem1  36712  hbtlem7  36714  rgspnval  36757  mendval  36772  cnvtrucl0  36950  eliunov2  36990  iunrelexpmin1  37019  iunrelexpmin2  37023  trclfvcom  37034  cnvtrclfv  37035  trclimalb2  37037  trclfvdecomr  37039  frege81d  37058  frege129d  37074  gneispacef2  37454  gneispacern2  37457  gneispace0nelrn  37458  addrval  37691  subrval  37692  mulvval  37693  elixpconstg  38294  dmmptdf  38412  upbdrech  38460  climf  38689  climf2  38733  dvcosre  38799  itgsinexplem1  38845  itgsubsticclem  38867  dmvolss  38878  stoweidlem26  38919  stoweidlem35  38928  stirlinglem14  38980  fourierdlem42  39042  fourierdlem81  39080  fourierdlem89  39088  fourierdlem91  39090  salgenval  39217  ismea  39344  afvprc  39873  pfxval  40246  mptmpt2opabbrd  40335  uvtxaval  40613  cplgr2vpr  40655  vtxdgfval  40683  1loopgrnb0  40717  ewlksfval  40803  1wlksfval  40811  wlksfval  40812  is1wlkg  40816  wwlksnon  41049  wspthsnon  41050  wlknwwlksnsur  41087  intopval  41628  clintopval  41630  assintopval  41631  isrngisom  41686  rngcvalALTV  41753  rngcval  41754  rnghmsscmap  41766  ringcvalALTV  41799  ringcval  41800  rhmsscmap  41812  dmatbas  41986  lincop  41991  lcoop  41994  offval0  42093  fdivval  42131  blenval  42163
  Copyright terms: Public domain W3C validator