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

Theorem elex 3243
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 1835 . 2 (∃𝑥(𝑥 = 𝐴𝑥𝐵) → ∃𝑥 𝑥 = 𝐴)
2 df-clel 2647 . 2 (𝐴𝐵 ↔ ∃𝑥(𝑥 = 𝐴𝑥𝐵))
3 isset 3238 . 2 (𝐴 ∈ V ↔ ∃𝑥 𝑥 = 𝐴)
41, 2, 33imtr4i 281 1 (𝐴𝐵𝐴 ∈ V)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383   = wceq 1523  wex 1744  wcel 2030  Vcvv 3231
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-12 2087  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-an 385  df-tru 1526  df-ex 1745  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-v 3233
This theorem is referenced by:  elexi  3244  elexd  3245  elisset  3246  prcnel  3249  vtoclgftOLD  3286  vtoclgf  3295  vtoclg1f  3296  vtocl2gf  3299  vtocl3gf  3300  spcimgft  3315  elab4g  3387  elrabf  3392  mob  3421  sbcex  3478  sbcel1v  3528  sbcabel  3550  csbiebt  3586  eldif  3617  ssv  3658  elun  3786  elin  3829  csbnestgf  4029  sbcco3g  4032  csbco3g  4033  csbvarg  4036  sbccsb2  4038  elpwb  4202  elpr2  4232  snidb  4240  ifpr  4265  eldifvsn  4359  elpreqpr  4427  dfopg  4431  eluni  4471  eliun  4556  csbexg  4825  nvel  4830  class2seteq  4863  axpweq  4872  reusv2lem4  4902  elopab  5012  epelg  5059  opelvvg  5199  opeliunxp2  5293  opelresg  5434  imasng  5522  elimasni  5527  iniseg  5531  inisegn0  5532  dmmptg  5670  elon2  5772  ordsssuc2  5852  iota2  5915  fnmptf  6054  fnmpt  6058  dmmptd  6062  elfvex  6259  fvelimab  6292  fvmptdv2  6337  mpteqb  6338  fvmptt  6339  fvmptf  6340  fvopab5  6349  fvopab6  6350  fprg  6462  fmptpr  6479  tpres  6507  eloprabga  6789  ovmpt2s  6826  ov2gf  6827  ovmpt2dxf  6828  ovmpt2x  6831  ovmpt2ga  6832  ovmpt2df  6834  ovmpt3rab1  6933  brrpssg  6981  sorpssi  6985  unexg  7001  elpwun  7019  ordeleqon  7030  onintrab  7043  sucexg  7052  ordsucelsuc  7064  onzsl  7088  elxp5  7153  offval3  7204  releldm2  7262  fnmpt2  7283  mpt2exg  7290  mptmpt2opabbrd  7293  offval22  7298  bropfvvvv  7302  suppval  7342  mptsuppd  7363  suppssov1  7372  suppssfv  7376  opeliunxp2f  7381  brtpos2  7403  undefval  7447  tfr2b  7537  tz7.49  7585  oeordi  7712  oeeu  7728  relelec  7830  ecdmn0  7832  mapvalg  7909  pmvalg  7910  elpmg  7915  elixp2  7954  mptelixpg  7987  elixpsn  7989  2pwuninel  8156  fival  8359  elfi2  8361  dffi2  8370  elfiun  8377  wemappo  8495  wemapso  8497  wemapso2lem  8498  harval  8508  brwdom  8513  fowdom  8517  brwdom2  8519  brwdom3  8528  en2lp  8548  cantnfsuc  8605  cnfcomlem  8634  rankvalb  8698  rankwflem  8716  rankr1g  8733  r1pwALT  8747  r1rankid  8760  cardval3  8816  pm54.43lem  8863  dfac8alem  8890  ac5num  8897  isacn  8905  numacn  8910  acndom  8912  cardinfima  8958  unialeph  8962  cdaval  9030  cflm  9110  isf32lem2  9214  isfin1-2  9245  itunifval  9276  numth3  9330  ttukeylem1  9369  ttukeylem3  9371  cardidg  9408  ondomon  9423  canth4  9507  canthnumlem  9508  canthwelem  9510  elwina  9546  elina  9547  wuncval  9602  grothpw  9686  tskmval  9699  eltskm  9703  recmulnq  9824  elnp  9847  elnpi  9848  npomex  9856  elfzp12  12457  mptnn0fsupp  12837  mptnn0fsuppr  12839  seqp1  12856  seqf1olem2  12881  hashinf  13162  hashxnn0  13167  hashnn0pnf  13170  hashxrcl  13186  prsshashgt1  13236  hashbclem  13274  lsw  13384  ccatfval  13391  ccats1alpha  13436  swrdval  13462  cats1un  13521  splval  13548  splcl  13549  revval  13555  reps  13563  s3sndisj  13752  s3iunsndisj  13753  trclfv  13785  relexp0g  13806  relexpsucnnr  13809  relexp1g  13810  limsupcl  14248  limsupval  14249  clim  14269  rlim  14270  fsumrlim  14587  hashbcval  15753  isstruct2  15914  strfvnd  15923  setsvalg  15934  setsfun0  15941  setscom  15950  strfv2d  15952  setsid  15961  ressval  15974  ressinbas  15983  restval  16134  prdsval  16162  prdssca  16163  pwsval  16193  imasval  16218  qusval  16249  xpsfrnel  16270  xpsfrnel2  16272  xpsval  16279  ismre  16297  oppcval  16420  brssc  16521  rescval  16534  issubc  16542  isfunc  16571  cofuval  16589  resfval  16599  funcres2c  16608  homadm  16737  homacd  16738  setcval  16774  catcval  16793  estrcval  16811  estrres  16826  xpcval  16864  prfval  16886  curfval  16910  uncfval  16921  pltfval  17006  pospo  17020  lubfval  17025  glbfval  17038  joinfval  17048  meetfval  17062  p0val  17088  p1val  17089  oduclatb  17191  ipoval  17201  ipodrsima  17212  prdsmndd  17370  prds0g  17371  pws0g  17373  frmdval  17435  vrmdfval  17440  prdsgrpd  17572  prdsinvgd  17573  eqgfval  17689  eqgval  17690  gaid  17778  cntzfval  17799  symgval  17845  elsymgbas  17848  symg2hash  17863  pmtrfval  17916  symggen  17936  gexval  18039  lsmfval  18099  pj1fval  18153  frgpval  18217  vrgpfval  18225  prdscmnd  18310  dmdprd  18443  dprdw  18455  pws1  18662  pwsmgp  18664  dvdsr  18692  isirred  18745  isrim0  18771  issrng  18898  lssset  18982  prdslmodd  19017  lspfval  19021  islbs  19124  sraval  19224  psrval  19410  mvrfval  19468  ltbval  19519  opsrval  19522  evlsval  19567  evlsval2  19568  coe1fval  19623  evls1fval  19732  zlmval  19912  psgnevpmb  19981  ocvfval  20058  cssval  20074  thlval  20087  dsmmval  20126  dsmmbase  20127  frlmval  20140  uvcfval  20171  elfilspd  20190  islinds  20196  mamufval  20239  matval  20265  oftpos  20306  dmatval  20346  scmatval  20358  mvmulfval  20396  smadiadetglem2  20526  cpmat  20562  mat2pmatfval  20576  cpm2mfval  20602  decpmatval0  20617  pm2mpval  20648  chpmatfval  20683  basdif0  20805  tgval  20807  eltg  20809  eltg2  20810  neipeltop  20981  islp  20992  ordtval  21041  dis2ndc  21311  islocfin  21368  txval  21415  qtopval  21546  elmptrab2  21679  isfbas  21680  isfildlem  21708  snfil  21715  cfinfil  21744  csdfil  21745  supfil  21746  fin1aufil  21783  fmval  21794  fmf  21796  isfcls  21860  alexsub  21896  alexsubb  21897  tsmsfbas  21978  tsmsval2  21980  ustval  22053  elutop  22084  isusp  22112  ispsmet  22156  ismet  22175  isxmet  22176  prdsdsf  22219  prdsxmet  22221  blfvalps  22235  metustel  22402  tngval  22490  elpi1  22891  rrxval  23221  itgfsum  23638  q1peqb  23959  ig1pval  23977  taylfval  24158  ulmval  24179  mtest  24203  iscgrg  25452  isismt  25474  legval  25524  ishlg  25542  mirval  25595  perpln1  25650  perpln2  25651  isperp  25652  ishpg  25696  midf  25713  ismidb  25715  lmif  25722  islmib  25724  iscgra  25746  isinag  25774  isleag  25778  iseqlg  25792  f1otrg  25796  f1otrge  25797  ttgval  25800  xmstrkgc  25811  vtxvalOLD  25925  iedgvalOLD  25926  edgvalOLD  25987  uvtxavalOLD  26334  cplgr2vpr  26385  vtxdgfval  26419  1loopgrnb0  26454  ewlksfval  26553  wksfval  26561  iswlkg  26565  wwlksnon  26800  wspthsnon  26801  wlknwwlksnsur  26844  avril1  27449  ispligb  27459  gidval  27494  isvcOLD  27562  0vfval  27589  elunop  28859  rabexgfGS  29466  disjdifprg  29514  disjdifprg2  29515  abfmpunirn  29580  rabfmpunirn  29581  funcnvmptOLD  29595  funcnvmpt  29596  fcobijfs  29629  sgnsv  29855  inftmrel  29862  isinftm  29863  resvval  29955  smatfval  29989  lmatval  30007  ispcmp  30052  qqhval2  30154  rrhval  30168  xrhval  30190  indv  30202  esumc  30241  esumpad  30245  esumpcvgval  30268  ofcfval  30288  ofcfval3  30292  issiga  30302  baselsiga  30306  sigasspw  30307  issgon  30314  isrnsigau  30318  sigagenval  30331  ispisys2  30344  cldssbrsiga  30378  sxval  30381  ismeas  30390  cnmbfm  30453  mbfmcnt  30458  omsfval  30484  elcarsg  30495  sitmval  30539  eulerpartlemt0  30559  sseqval  30578  sseqmw  30581  sseqp1  30585  orvcval  30647  orvcval4  30650  ballotlemsv  30699  mrexval  31524  mrsubffval  31530  msubffval  31546  mclsval  31586  eldm3  31777  opelco3  31802  elima4  31803  elno  31924  nosupno  31974  noetalem5  31992  nulsslt  32033  nulssgt  32034  elfix2  32136  elsingles  32150  fvimage  32163  funpartlem  32174  elaltxp  32207  brcolinear2  32290  ellines  32384  topfneec  32475  topfneec2  32476  fnejoin2  32489  limsucncmpi  32569  findabrcl  32578  bj-sngltag  33096  bj-xtagex  33102  bj-evalval  33152  bj-ismoorec  33185  bj-diagval  33220  bj-eldiag2  33222  finxpreclem1  33356  finxpreclem3  33360  poimirlem17  33556  opelopab3  33641  elghomlem2OLD  33815  isrngo  33826  isdivrngo  33879  opelresALTV  34172  cnvepresex  34245  riotasv2d  34561  riotasv3d  34564  lshpset  34583  lsatset  34595  lcvfbr  34625  lflset  34664  lkrfval  34692  lkrval2  34695  islshpkrN  34725  ldualset  34730  cmtfvalN  34815  cvrfval  34873  pats  34890  llnset  35109  lplnset  35133  lvolset  35176  lineset  35342  pointsetN  35345  psubspset  35348  pmapfval  35360  paddfval  35401  pclfvalN  35493  polfvalN  35508  psubclsetN  35540  watfvalN  35596  lhpset  35599  lautset  35686  pautsetN  35702  ldilfset  35712  ltrnfset  35721  dilfsetN  35757  trnfsetN  35760  trlfset  35765  tgrpfset  36349  tendofset  36363  erngfset  36404  erngfset-rN  36412  dvafset  36609  diaffval  36636  dvhfset  36686  docaffvalN  36727  djaffvalN  36739  dibffval  36746  dicffval  36780  dihffval  36836  dochffval  36955  djhffval  37002  lpolsetN  37088  lcdfval  37194  mapdffval  37232  hvmapffval  37364  hdmap1ffval  37402  hdmapffval  37435  hgmapffval  37494  hlhilset  37543  elrfi  37574  nacsfix  37592  mapfzcons2  37599  sbc2rexgOLD  37669  sbc4rexgOLD  37671  setindtrs  37909  wepwso  37930  hbtlem1  38010  hbtlem7  38012  rgspnval  38055  mendval  38070  cnvtrucl0  38248  eliunov2  38288  iunrelexpmin1  38317  iunrelexpmin2  38321  trclfvcom  38332  cnvtrclfv  38333  trclimalb2  38335  trclfvdecomr  38337  frege81d  38356  frege129d  38372  gneispacef2  38751  gneispacern2  38754  gneispace0nelrn  38755  addrval  38987  subrval  38988  mulvval  38989  elixpconstg  39580  dmmptdf  39731  dmmptdf2  39753  mptfnd  39765  upbdrech  39833  climf  40172  climf2  40216  liminfval  40309  dvcosre  40444  itgsinexplem1  40487  itgsubsticclem  40509  dmvolss  40520  stoweidlem26  40561  stoweidlem35  40570  stirlinglem14  40622  fourierdlem42  40684  fourierdlem81  40722  fourierdlem89  40730  fourierdlem91  40732  salgenval  40859  ismea  40986  pfxval  41708  upwlksfval  42041  isupwlkg  42043  elsprel  42050  sprval  42054  intopval  42163  clintopval  42165  assintopval  42166  isrngisom  42221  rngcvalALTV  42286  rngcval  42287  rnghmsscmap  42299  ringcvalALTV  42332  ringcval  42333  rhmsscmap  42345  dmatbas  42517  lincop  42522  lcoop  42525  offval0  42624  fdivval  42658  blenval  42690
  Copyright terms: Public domain W3C validator