MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  elpw Unicode version

Theorem elpw 3572
Description: Membership in a power class. Theorem 86 of [Suppes] p. 47. (Contributed by NM, 31-Dec-1993.)
Hypothesis
Ref Expression
elpw.1  |-  A  e. 
_V
Assertion
Ref Expression
elpw  |-  ( A  e.  ~P B  <->  A  C_  B
)

Proof of Theorem elpw
StepHypRef Expression
1 elpw.1 . 2  |-  A  e. 
_V
2 sseq1 3141 . 2  |-  ( x  =  A  ->  (
x  C_  B  <->  A  C_  B
) )
3 df-pw 3568 . 2  |-  ~P B  =  { x  |  x 
C_  B }
41, 2, 3elab2 2868 1  |-  ( A  e.  ~P B  <->  A  C_  B
)
Colors of variables: wff set class
Syntax hints:    <-> wb 178    e. wcel 1621   _Vcvv 2740    C_ wss 3094   ~Pcpw 3566
This theorem is referenced by:  elpwg  3573  prsspw  3726  pwpr  3764  pwtp  3765  pwv  3767  sspwuni  3928  iinpw  3931  iunpwss  3932  0elpw  4118  pwuni  4144  snelpwi  4158  snelpw  4159  sspwb  4161  ssextss  4165  pwin  4234  pwunss  4235  pwssun  4236  pwundifOLD  4238  iunpw  4507  ordpwsuc  4543  xpsspw  4750  xpsspwOLD  4751  fabexg  5325  knatar  5756  sorpsscmpl  6187  qsss  6653  mapval2  6730  pmsspw  6735  uniixp  6772  fopwdom  6903  ssenen  6968  fineqvlem  7010  fissuni  7093  fipreima  7094  fival  7099  fiin  7108  fipwuni  7112  dffi3  7117  marypha1lem  7119  hartogslem1  7190  inf3lem6  7267  tz9.12lem3  7394  rankonidlem  7433  tskwe  7516  r0weon  7573  infpwfien  7622  dfac5lem4  7686  dfac2  7690  dfac12lem2  7703  ackbij2lem3  7800  cfval2  7819  fin23lem11  7876  enfin2i  7880  compsscnvlem  7929  isfin1-3  7945  fin1a2lem13  7971  itunitc1  7979  hsmexlem4  7988  hsmexlem5  7989  axdc3lem  8009  axdc4lem  8014  fpwwe2lem1  8186  fpwwe2lem11  8195  fpwwe2lem12  8196  fpwwe  8201  canthwe  8206  pwfseqlem1  8213  eltsk2g  8306  axgroth5  8379  axgroth6  8383  wuncn  8725  ixxssxr  10599  ioof  10672  fzof  10803  hashbclem  11320  vdwmc  12952  ramub2  12988  ram0  12996  ramub1lem1  13000  ramub1lem2  13001  restsspw  13263  prdsplusg  13285  prdsmulr  13286  prdsvsca  13287  ismred  13431  mremre  13433  submrc  13457  isacs2  13482  mreacs  13487  acsfn  13488  isssc  13624  homaf  13789  catcfuccl  13868  catcxpccl  13908  isdrs2  14000  fpwipodrs  14194  isacs4lem  14198  isacs5lem  14199  submacs  14369  subgacs  14579  nsgacs  14580  sylow2alem2  14856  sylow2a  14857  sylow3lem3  14867  sylow3lem6  14870  dprdres  15190  subgdmdprd  15196  dprd2dlem1  15203  ablfac1b  15232  pgpfac1lem5  15241  subrgmre  15496  subsubrg2  15499  lssintcl  15648  lssmre  15650  lssacs  15651  cssval  16509  cssmre  16520  istopon  16590  tgval2  16621  tgdom  16643  distop  16660  fctop  16668  cctop  16670  ppttop  16671  pptbas  16672  epttop  16673  cldss2  16694  ntreq0  16741  discld  16753  mretopd  16756  toponmre  16757  neisspw  16771  resttopon  16819  restdis  16836  cnntr  16931  isnrm2  17013  dishaus  17037  cmpcovf  17045  fincmp  17047  discmp  17052  cmpsublem  17053  cmpsub  17054  cmpcld  17056  cmpfi  17062  concompid  17084  is1stc2  17095  2ndcdisj  17109  2ndcsep  17112  llyi  17127  nllyi  17128  nlly2i  17129  llynlly  17130  subislly  17134  restnlly  17135  llyrest  17138  llyidm  17141  nllyidm  17142  cldllycmp  17148  dislly  17150  iskgen3  17171  kgencn2  17179  txuni2  17187  ptuni2  17198  dfac14  17239  prdstopn  17249  txcmplem1  17262  txcmplem2  17263  qtoptop2  17317  qtopuni  17320  tgqtop  17330  hmphdis  17414  isfbas2  17457  fbssfi  17459  trfbas2  17465  isfild  17480  elfg  17493  cfinfil  17515  csdfil  17516  supfil  17517  isufil2  17530  filssufilg  17533  uffix  17543  uffixsn  17547  ufildr  17553  fin1aufil  17554  hauspwpwf1  17609  alexsubb  17667  alexsubALTlem1  17668  alexsubALTlem2  17669  alexsubALT  17672  ptcmplem5  17677  cldsubg  17720  met1stc  17994  dscopn  18023  icccmplem1  18254  icccmplem2  18255  opnmbllem  18883  vitali  18895  sqff1o  20347  sspval  21224  shex  21716  dfch2  21911  ballotlem2  22973  ballotth  23022  erdszelem7  23065  erdsze2lem2  23072  rellyscon  23119  cvmcov2  23143  umgra1  23215  eupath2  23241  dffr5  23446  elfuns  23794  altxpsspw  23851  elhf2  24145  svs2  24819  sallnei  24861  qusp  24874  fgsb2  24887  bwt2  24924  intvconlem1  25035  issubcata  25178  tartarmap  25220  pgapspf  25384  islocfin  25628  neibastop1  25640  neibastop2lem  25641  neibastop3  25643  topmeet  25645  topjoin  25646  neifg  25652  heibor1lem  25865  heiborlem1  25867  heiborlem8  25874  elrfi  26101  ismrcd1  26105  ismrcd2  26106  istopclsd  26107  mrefg2  26114  isnacs3  26117  pw2f1ocnv  26462  dfac11  26492  islssfg2  26501  filnm  26524  lnr2i  26652  hbtlem6  26665  sdrgacs  26841  stoweidlem57  27106  trsspwALT  27605  trsspwALT2  27606  trsspwALT3  27607  pwtrVD  27611  pwtrOLD  27612  pclfinN  29219  lcdlss  30939  mapd1o  30968
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1927  ax-ext 2237
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1884  df-clab 2243  df-cleq 2249  df-clel 2252  df-nfc 2381  df-v 2742  df-in 3101  df-ss 3108  df-pw 3568
  Copyright terms: Public domain W3C validator