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

Theorem elpw 3807
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
Dummy variable  x is distinct from all other variables.
StepHypRef Expression
1 elpw.1 . 2  |-  A  e. 
_V
2 sseq1 3371 . 2  |-  ( x  =  A  ->  (
x  C_  B  <->  A  C_  B
) )
3 df-pw 3803 . 2  |-  ~P B  =  { x  |  x 
C_  B }
41, 2, 3elab2 3087 1  |-  ( A  e.  ~P B  <->  A  C_  B
)
Colors of variables: wff set class
Syntax hints:    <-> wb 178    e. wcel 1726   _Vcvv 2958    C_ wss 3322   ~Pcpw 3801
This theorem is referenced by:  elpwg  3808  prsspw  3973  pwpr  4013  pwtp  4014  pwv  4016  sspwuni  4178  iinpw  4181  iunpwss  4182  0elpw  4371  pwuni  4397  snelpwi  4411  snelpw  4412  prelpwi  4413  sspwb  4415  ssextss  4419  pwin  4489  pwunss  4490  pwssun  4491  iunpw  4761  ordpwsuc  4797  xpsspw  4988  xpsspwOLD  4989  fabexg  5626  knatar  6082  sorpsscmpl  6535  qsss  6967  mapval2  7045  pmsspw  7050  uniixp  7087  ssenen  7283  fineqvlem  7325  fissuni  7413  fipreima  7414  fival  7419  fiin  7429  fipwuni  7433  dffi3  7438  marypha1lem  7440  hartogslem1  7513  inf3lem6  7590  tz9.12lem3  7717  rankonidlem  7756  tskwe  7839  r0weon  7896  infpwfien  7945  dfac5lem4  8009  dfac2  8013  dfac12lem2  8026  cfval2  8142  enfin2i  8203  compsscnvlem  8252  isfin1-3  8268  fin1a2lem13  8294  itunitc1  8302  hsmexlem4  8311  hsmexlem5  8312  axdc3lem  8332  axdc4lem  8337  fpwwe2lem1  8508  fpwwe2lem11  8517  fpwwe2lem12  8518  fpwwe  8523  canthwe  8528  pwfseqlem1  8535  eltsk2g  8628  axgroth5  8701  axgroth6  8705  wuncn  9047  ixxssxr  10930  ioof  11004  fzof  11139  hashbclem  11703  incexclem  12618  vdwmc  13348  ramub2  13384  ram0  13392  ramub1lem1  13396  ramub1lem2  13397  restsspw  13661  prdsplusg  13683  prdsmulr  13684  prdsvsca  13685  ismred  13829  mremre  13831  submrc  13855  isacs2  13880  mreacs  13885  acsfn  13886  isssc  14022  homaf  14187  catcfuccl  14266  catcxpccl  14306  fpwipodrs  14592  isacs4lem  14596  isacs5lem  14597  submacs  14767  subgacs  14977  nsgacs  14978  sylow2alem2  15254  sylow2a  15255  sylow3lem3  15265  sylow3lem6  15268  dprdres  15588  subgdmdprd  15594  dprd2dlem1  15601  ablfac1b  15630  pgpfac1lem5  15639  subrgmre  15894  subsubrg2  15897  lssintcl  16042  lssmre  16044  lssacs  16045  cssval  16911  cssmre  16922  istopon  16992  tgval2  17023  tgdom  17045  distop  17062  fctop  17070  cctop  17072  ppttop  17073  pptbas  17074  epttop  17075  cldss2  17096  ntreq0  17143  discld  17155  mretopd  17158  toponmre  17159  neisspw  17173  resttopon  17227  restdis  17244  cnntr  17341  isnrm2  17424  dishaus  17448  cmpcovf  17456  fincmp  17458  discmp  17463  cmpsublem  17464  cmpsub  17465  cmpcld  17467  cmpfi  17473  bwth  17475  concompid  17496  is1stc2  17507  2ndcdisj  17521  2ndcsep  17524  llyi  17539  nllyi  17540  nlly2i  17541  llynlly  17542  subislly  17546  restnlly  17547  llyrest  17550  llyidm  17553  nllyidm  17554  cldllycmp  17560  dislly  17562  iskgen3  17583  kgencn2  17591  txuni2  17599  ptuni2  17610  dfac14  17652  prdstopn  17662  txcmplem1  17675  txcmplem2  17676  qtoptop2  17733  qtopuni  17736  tgqtop  17746  hmphdis  17830  isfbas2  17869  fbssfi  17871  trfbas2  17877  isfild  17892  elfg  17905  cfinfil  17927  csdfil  17928  supfil  17929  isufil2  17942  filssufilg  17945  uffix  17955  uffixsn  17959  ufildr  17965  fin1aufil  17966  hauspwpwf1  18021  alexsubb  18079  alexsubALTlem1  18080  alexsubALTlem2  18081  alexsubALT  18084  ptcmplem5  18089  cldsubg  18142  ustfn  18233  ustn0  18252  met1stc  18553  restmetu  18619  dscopn  18623  icccmplem1  18855  icccmplem2  18856  opnmbllem  19495  vitali  19507  sqff1o  20967  umgra1  21363  uslgra1  21394  usgraedgrnv  21399  usgrarnedg  21406  usgraedg4  21408  usgrares1  21426  cusgrarn  21470  eupath2  21704  sspval  22224  shex  22716  dfch2  22911  ishashinf  24161  esumpcvgval  24470  esumcvg  24478  sigaex  24494  sigaval  24495  pwsiga  24515  difelsiga  24518  sigainb  24521  insiga  24522  measssd  24571  measdivcst  24581  cntnevol  24584  mbfmcnt  24620  br2base  24621  sxbrsigalem0  24623  probun  24679  coinfliprv  24742  ballotlem2  24748  ballotth  24797  erdszelem7  24885  erdsze2lem2  24892  rellyscon  24940  cvmcov2  24964  dffr5  25378  elfuns  25762  altxpsspw  25824  elhf2  26118  opnmbllem0  26244  islocfin  26378  neibastop1  26390  neibastop2lem  26391  neibastop3  26393  topmeet  26395  topjoin  26396  neifg  26402  heibor1lem  26520  heiborlem1  26522  heiborlem8  26529  elrfi  26750  ismrcd1  26754  ismrcd2  26755  istopclsd  26756  mrefg2  26763  isnacs3  26766  pw2f1ocnv  27110  dfac11  27139  islssfg2  27148  filnm  27171  lnr2i  27299  hbtlem6  27312  sdrgacs  27488  stoweidlem57  27784  trsspwALT  28993  trsspwALT2  28994  trsspwALT3  28995  pwtrVD  28999  pclfinN  30759  lcdlss  32479  mapd1o  32508
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-v 2960  df-in 3329  df-ss 3336  df-pw 3803
  Copyright terms: Public domain W3C validator