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

Theorem elex 3404
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 1956 . 2 (∃𝑥(𝑥 = 𝐴𝑥𝐵) → ∃𝑥 𝑥 = 𝐴)
2 df-clel 2800 . 2 (𝐴𝐵 ↔ ∃𝑥(𝑥 = 𝐴𝑥𝐵))
3 isset 3399 . 2 (𝐴 ∈ V ↔ ∃𝑥 𝑥 = 𝐴)
41, 2, 33imtr4i 283 1 (𝐴𝐵𝐴 ∈ V)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384   = wceq 1637  wex 1859  wcel 2156  Vcvv 3389
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-12 2214  ax-ext 2782
This theorem depends on definitions:  df-bi 198  df-an 385  df-tru 1641  df-ex 1860  df-sb 2061  df-clab 2791  df-cleq 2797  df-clel 2800  df-v 3391
This theorem is referenced by:  elexi  3405  elexd  3406  elisset  3407  prcnel  3410  vtoclgf  3455  vtoclg1f  3456  vtocl2gf  3459  vtocl3gf  3460  spcimgft  3475  elab4g  3548  elrabf  3553  mob  3584  sbcex  3641  sbcel1v  3690  sbcabel  3710  csbiebt  3746  eldif  3777  ssv  3820  elun  3950  elin  3993  csbnestgf  4191  sbcco3g  4194  csbco3g  4195  csbvarg  4198  sbccsb2  4201  ifexg  4324  elpwb  4360  elpr2  4392  snidb  4399  ifpr  4423  eldifvsn  4516  prnesn  4579  elpreqpr  4587  dfopg  4591  eluni  4631  eliun  4714  csbexg  4985  nvel  4991  class2seteq  5023  axpweq  5032  reusv2lem4  5068  opeqsng  5154  elopab  5176  epelg  5223  opelvvg  5363  opeliunxp2  5460  opelresg  5601  imasng  5695  elimasni  5700  iniseg  5704  inisegn0  5705  dmmptg  5844  elon2  5945  ordsssuc2  6025  iota2  6088  fnmptf  6225  fnmpt  6229  dmmptd  6233  elfvex  6439  fvelimab  6472  fvmptdv2  6517  mpteqb  6518  fvmptt  6519  fvmptf  6520  fvopab5  6529  fvopab6  6530  fprg  6644  fmptpr  6661  tpres  6689  eloprabga  6975  ovmpt2s  7012  ov2gf  7013  ovmpt2dxf  7014  ovmpt2x  7017  ovmpt2ga  7018  ovmpt2df  7020  ovmpt3rab1  7119  brrpssg  7167  sorpssi  7171  unexg  7187  elpwun  7205  ordeleqon  7216  onintrab  7229  sucexg  7238  ordsucelsuc  7250  onzsl  7274  elxp5  7339  offval3  7390  releldm2  7448  fnmpt2  7469  mpt2exg  7476  mptmpt2opabbrd  7479  offval22  7485  bropfvvvv  7489  suppval  7529  mptsuppd  7550  suppssov1  7560  suppssfv  7564  opeliunxp2f  7569  brtpos2  7591  undefval  7635  tfr2b  7726  tz7.49  7774  oeordi  7902  oeeu  7918  relelec  8020  ecdmn0  8022  mapvalg  8100  pmvalg  8101  elpmg  8106  elixp2  8147  mptelixpg  8180  elixpsn  8182  snmapen  8271  2pwuninel  8352  fival  8555  elfi2  8557  dffi2  8566  elfiun  8573  wemappo  8691  wemapso  8693  wemapso2lem  8694  harval  8704  brwdom  8709  fowdom  8713  brwdom2  8715  brwdom3  8724  en2lp  8747  cantnfsuc  8812  cnfcomlem  8841  rankvalb  8905  rankwflem  8923  rankr1g  8940  r1pwALT  8954  r1rankid  8967  djulcl  9017  djurcl  9018  inlresf  9021  inrresf  9023  djuss  9027  1stinl  9034  2ndinl  9035  1stinr  9036  2ndinr  9037  cardval3  9059  pm54.43lem  9106  dfac8alem  9133  ac5num  9140  isacn  9148  numacn  9153  acndom  9155  cardinfima  9201  unialeph  9205  cdaval  9275  ackbij1lem5  9329  cflm  9355  isf32lem2  9459  isfin1-2  9490  itunifval  9521  numth3  9575  ttukeylem1  9614  ttukeylem3  9616  cardidg  9653  ondomon  9668  canth4  9752  canthnumlem  9753  canthwelem  9755  elwina  9791  elina  9792  wuncval  9847  grothpw  9931  tskmval  9944  eltskm  9948  recmulnq  10069  elnp  10092  elnpi  10093  npomex  10101  elfzp12  12640  mptnn0fsupp  13018  mptnn0fsuppr  13020  seqp1  13037  seqf1olem2  13062  hashinf  13340  hashxnn0  13345  hashnn0pnf  13348  hashxrcl  13364  prsshashgt1  13413  hashmap  13437  hashbclem  13451  lsw  13561  ccatfval  13568  ccats1alpha  13612  swrdval  13638  cats1un  13697  splval  13724  splcl  13725  revval  13731  reps  13739  s3sndisj  13929  s3iunsndisj  13930  trclfv  13962  relexp0g  13983  relexpsucnnr  13986  relexp1g  13987  limsupcl  14425  limsupval  14426  clim  14446  rlim  14447  fsumrlim  14763  hashbcval  15921  isstruct2  16076  strfvnd  16085  setsvalg  16096  setsfun0  16103  setscom  16112  strfv2d  16114  setsid  16123  ressval  16136  ressinbas  16145  restval  16290  prdsval  16318  prdssca  16319  pwsval  16349  imasval  16374  qusval  16405  xpsfrnel  16426  xpsfrnel2  16428  xpsval  16435  ismre  16453  oppcval  16575  brssc  16676  rescval  16689  issubc  16697  isfunc  16726  cofuval  16744  resfval  16754  funcres2c  16763  homadm  16892  homacd  16893  setcval  16929  catcval  16948  estrcval  16966  estrresOLD  16981  xpcval  17020  prfval  17042  curfval  17066  uncfval  17077  pltfval  17162  pospo  17176  lubfval  17181  glbfval  17194  joinfval  17204  meetfval  17218  p0val  17244  p1val  17245  oduclatb  17347  ipoval  17357  ipodrsima  17368  prdsmndd  17526  prds0g  17527  pws0g  17529  frmdval  17591  vrmdfval  17596  prdsgrpd  17728  prdsinvgd  17729  eqgfval  17842  eqgval  17843  gaid  17931  cntzfval  17952  symgval  17998  elsymgbas  18001  symg2hash  18016  pmtrfval  18069  symggen  18089  gexval  18192  lsmfval  18252  pj1fval  18306  frgpval  18370  vrgpfval  18378  prdscmnd  18463  dmdprd  18597  dprdw  18609  pws1  18816  pwsmgp  18818  dvdsr  18846  isirred  18899  isrim0  18925  issrng  19052  lssset  19136  prdslmodd  19174  lspfval  19178  islbs  19281  sraval  19383  psrval  19569  mvrfval  19627  ltbval  19678  opsrval  19681  evlsval  19725  evlsval2  19726  coe1fval  19781  evls1fval  19890  zlmval  20070  psgnevpmb  20138  ocvfval  20218  cssval  20234  thlval  20247  dsmmval  20286  dsmmbase  20287  frlmval  20300  uvcfval  20331  elfilspd  20350  islinds  20356  mamufval  20399  matval  20425  oftpos  20467  dmatval  20507  scmatval  20519  mvmulfval  20557  smadiadetglem2  20688  cpmat  20725  mat2pmatfval  20739  cpm2mfval  20765  decpmatval0  20780  pm2mpval  20811  chpmatfval  20846  basdif0  20969  tgval  20971  eltg  20973  eltg2  20974  neipeltop  21145  islp  21156  ordtval  21205  dis2ndc  21475  islocfin  21532  txval  21579  qtopval  21710  elmptrab2  21843  isfbas  21844  isfildlem  21872  snfil  21879  cfinfil  21908  csdfil  21909  supfil  21910  fin1aufil  21947  fmval  21958  fmf  21960  isfcls  22024  alexsub  22060  alexsubb  22061  tsmsfbas  22142  tsmsval2  22144  ustval  22217  elutop  22248  isusp  22276  ispsmet  22320  ismet  22339  isxmet  22340  prdsdsf  22383  prdsxmet  22385  blfvalps  22399  metustel  22566  tngval  22654  elpi1  23055  rrxval  23385  itgfsum  23805  q1peqb  24126  ig1pval  24144  taylfval  24325  ulmval  24346  mtest  24370  iscgrg  25619  isismt  25641  legval  25691  ishlg  25709  mirval  25762  perpln1  25817  perpln2  25818  isperp  25819  ishpg  25863  midf  25880  ismidb  25882  lmif  25889  islmib  25891  iscgra  25913  isinag  25941  isleag  25945  iseqlg  25959  f1otrg  25963  f1otrge  25964  ttgval  25967  xmstrkgc  25978  vtxvalOLD  26092  iedgvalOLD  26093  edgvalOLD  26154  uvtxavalOLD  26504  cplgr2vpr  26555  vtxdgfval  26589  1loopgrnb0  26624  ewlksfval  26723  wksfval  26731  iswlkg  26735  wwlksnon  26971  wspthsnon  26972  wlknwwlksnsurOLD  27015  avril1  27648  ispligb  27658  gidval  27693  isvcOLD  27760  0vfval  27787  elunop  29057  rabexgfGS  29663  disjdifprg  29711  disjdifprg2  29712  abfmpunirn  29777  rabfmpunirn  29778  funcnvmptOLD  29792  funcnvmpt  29793  fcobijfs  29826  sgnsv  30050  inftmrel  30057  isinftm  30058  resvval  30150  smatfval  30184  lmatval  30202  ispcmp  30247  qqhval2  30349  rrhval  30363  xrhval  30385  indv  30397  esumc  30436  esumpad  30440  esumpcvgval  30463  ofcfval  30483  ofcfval3  30487  issiga  30497  baselsiga  30501  sigasspw  30502  issgon  30509  isrnsigau  30513  sigagenval  30526  ispisys2  30539  cldssbrsiga  30573  sxval  30576  ismeas  30585  cnmbfm  30648  mbfmcnt  30653  omsfval  30679  elcarsg  30690  sitmval  30734  eulerpartlemt0  30754  sseqval  30773  sseqmw  30776  sseqp1  30780  orvcval  30842  orvcval4  30845  ballotlemsv  30894  mrexval  31719  mrsubffval  31725  msubffval  31741  mclsval  31781  eldm3  31971  opelco3  31996  elima4  31997  elno  32118  nosupno  32168  noetalem5  32186  nulsslt  32227  nulssgt  32228  elfix2  32330  elsingles  32344  fvimage  32357  funpartlem  32368  elaltxp  32401  brcolinear2  32484  ellines  32578  topfneec  32669  topfneec2  32670  fnejoin2  32683  limsucncmpi  32759  findabrcl  32768  bj-sngltag  33279  bj-xtagex  33285  bj-evalval  33336  bj-ismoorec  33369  bj-diagval  33405  bj-eldiag2  33407  finxpreclem1  33540  finxpreclem3  33544  poimirlem17  33737  opelopab3  33821  elghomlem2OLD  33994  isrngo  34005  isdivrngo  34058  opelresALTV  34347  cnvepresex  34417  riotasv2d  34734  riotasv3d  34737  lshpset  34756  lsatset  34768  lcvfbr  34798  lflset  34837  lkrfval  34865  lkrval2  34868  islshpkrN  34898  ldualset  34903  cmtfvalN  34988  cvrfval  35046  pats  35063  llnset  35283  lplnset  35307  lvolset  35350  lineset  35516  pointsetN  35519  psubspset  35522  pmapfval  35534  paddfval  35575  pclfvalN  35667  polfvalN  35682  psubclsetN  35714  watfvalN  35770  lhpset  35773  lautset  35860  pautsetN  35876  ldilfset  35886  ltrnfset  35895  dilfsetN  35931  trnfsetN  35934  trlfset  35939  tgrpfset  36523  tendofset  36537  erngfset  36578  erngfset-rN  36586  dvafset  36783  diaffval  36809  dvhfset  36859  docaffvalN  36900  djaffvalN  36912  dibffval  36919  dicffval  36953  dihffval  37009  dochffval  37128  djhffval  37175  lpolsetN  37261  lcdfval  37367  mapdffval  37405  hvmapffval  37537  hdmap1ffval  37574  hdmapffval  37605  hgmapffval  37664  hlhilset  37713  elrfi  37757  nacsfix  37775  mapfzcons2  37782  sbc2rexgOLD  37852  sbc4rexgOLD  37854  setindtrs  38091  wepwso  38112  hbtlem1  38192  hbtlem7  38194  rgspnval  38237  mendval  38252  cnvtrucl0  38429  eliunov2  38469  iunrelexpmin1  38498  iunrelexpmin2  38502  trclfvcom  38513  cnvtrclfv  38514  trclimalb2  38516  trclfvdecomr  38518  frege81d  38537  frege129d  38553  gneispacef2  38932  gneispacern2  38935  gneispace0nelrn  38936  addrval  39166  subrval  39167  mulvval  39168  elixpconstg  39757  dmmptdf  39902  dmmptdf2  39921  mptfnd  39933  upbdrech  39998  climf  40332  climf2  40376  liminfval  40469  dvcosre  40604  itgsinexplem1  40647  itgsubsticclem  40668  dmvolss  40679  stoweidlem26  40720  stoweidlem35  40729  stirlinglem14  40781  fourierdlem42  40843  fourierdlem81  40881  fourierdlem89  40889  fourierdlem91  40891  salgenval  41018  ismea  41145  pfxval  41956  upwlksfval  42282  isupwlkg  42284  elsprel  42291  sprval  42295  intopval  42404  clintopval  42406  assintopval  42407  isrngisom  42462  rngcvalALTV  42527  rngcval  42528  rnghmsscmap  42540  ringcvalALTV  42573  ringcval  42574  rhmsscmap  42586  dmatbas  42758  lincop  42763  lcoop  42766  offval0  42865  fdivval  42899  blenval  42931
  Copyright terms: Public domain W3C validator