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

Theorem elpw 3631
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 3199 . 2  |-  ( x  =  A  ->  (
x  C_  B  <->  A  C_  B
) )
3 df-pw 3627 . 2  |-  ~P B  =  { x  |  x 
C_  B }
41, 2, 3elab2 2917 1  |-  ( A  e.  ~P B  <->  A  C_  B
)
Colors of variables: wff set class
Syntax hints:    <-> wb 176    e. wcel 1684   _Vcvv 2788    C_ wss 3152   ~Pcpw 3625
This theorem is referenced by:  elpwg  3632  prsspw  3785  pwpr  3823  pwtp  3824  pwv  3826  sspwuni  3987  iinpw  3990  iunpwss  3991  0elpw  4180  pwuni  4206  snelpwi  4220  snelpw  4221  sspwb  4223  ssextss  4227  pwin  4297  pwunss  4298  pwssun  4299  pwundifOLD  4301  iunpw  4570  ordpwsuc  4606  xpsspw  4797  xpsspwOLD  4798  fabexg  5422  knatar  5857  sorpsscmpl  6288  qsss  6720  mapval2  6797  pmsspw  6802  uniixp  6839  fopwdom  6970  ssenen  7035  fineqvlem  7077  fissuni  7160  fipreima  7161  fival  7166  fiin  7175  fipwuni  7179  dffi3  7184  marypha1lem  7186  hartogslem1  7257  inf3lem6  7334  tz9.12lem3  7461  rankonidlem  7500  tskwe  7583  r0weon  7640  infpwfien  7689  dfac5lem4  7753  dfac2  7757  dfac12lem2  7770  ackbij2lem3  7867  cfval2  7886  fin23lem11  7943  enfin2i  7947  compsscnvlem  7996  isfin1-3  8012  fin1a2lem13  8038  itunitc1  8046  hsmexlem4  8055  hsmexlem5  8056  axdc3lem  8076  axdc4lem  8081  fpwwe2lem1  8253  fpwwe2lem11  8262  fpwwe2lem12  8263  fpwwe  8268  canthwe  8273  pwfseqlem1  8280  eltsk2g  8373  axgroth5  8446  axgroth6  8450  wuncn  8792  ixxssxr  10668  ioof  10741  fzof  10872  hashbclem  11390  incexclem  12295  vdwmc  13025  ramub2  13061  ram0  13069  ramub1lem1  13073  ramub1lem2  13074  restsspw  13336  prdsplusg  13358  prdsmulr  13359  prdsvsca  13360  ismred  13504  mremre  13506  submrc  13530  isacs2  13555  mreacs  13560  acsfn  13561  isssc  13697  homaf  13862  catcfuccl  13941  catcxpccl  13981  isdrs2  14073  fpwipodrs  14267  isacs4lem  14271  isacs5lem  14272  submacs  14442  subgacs  14652  nsgacs  14653  sylow2alem2  14929  sylow2a  14930  sylow3lem3  14940  sylow3lem6  14943  dprdres  15263  subgdmdprd  15269  dprd2dlem1  15276  ablfac1b  15305  pgpfac1lem5  15314  subrgmre  15569  subsubrg2  15572  lssintcl  15721  lssmre  15723  lssacs  15724  cssval  16582  cssmre  16593  istopon  16663  tgval2  16694  tgdom  16716  distop  16733  fctop  16741  cctop  16743  ppttop  16744  pptbas  16745  epttop  16746  cldss2  16767  ntreq0  16814  discld  16826  mretopd  16829  toponmre  16830  neisspw  16844  resttopon  16892  restdis  16909  cnntr  17004  isnrm2  17086  dishaus  17110  cmpcovf  17118  fincmp  17120  discmp  17125  cmpsublem  17126  cmpsub  17127  cmpcld  17129  cmpfi  17135  concompid  17157  is1stc2  17168  2ndcdisj  17182  2ndcsep  17185  llyi  17200  nllyi  17201  nlly2i  17202  llynlly  17203  subislly  17207  restnlly  17208  llyrest  17211  llyidm  17214  nllyidm  17215  cldllycmp  17221  dislly  17223  iskgen3  17244  kgencn2  17252  txuni2  17260  ptuni2  17271  dfac14  17312  prdstopn  17322  txcmplem1  17335  txcmplem2  17336  qtoptop2  17390  qtopuni  17393  tgqtop  17403  hmphdis  17487  isfbas2  17530  fbssfi  17532  trfbas2  17538  isfild  17553  elfg  17566  cfinfil  17588  csdfil  17589  supfil  17590  isufil2  17603  filssufilg  17606  uffix  17616  uffixsn  17620  ufildr  17626  fin1aufil  17627  hauspwpwf1  17682  alexsubb  17740  alexsubALTlem1  17741  alexsubALTlem2  17742  alexsubALT  17745  ptcmplem5  17750  cldsubg  17793  met1stc  18067  dscopn  18096  icccmplem1  18327  icccmplem2  18328  opnmbllem  18956  vitali  18968  sqff1o  20420  sspval  21299  shex  21791  dfch2  21986  ballotlem2  23047  ballotth  23096  cntnevol  23175  esumel  23426  esumpcvgval  23446  esumcvg  23454  insiga  23498  measssd  23543  mbfmcnt  23573  br2base  23574  coinfliplem  23679  coinflippv  23684  erdszelem7  23728  erdsze2lem2  23735  rellyscon  23782  cvmcov2  23806  umgra1  23878  eupath2  23904  dffr5  24110  elfuns  24454  altxpsspw  24511  elhf2  24805  svs2  25487  sallnei  25529  qusp  25542  fgsb2  25555  bwt2  25592  intvconlem1  25703  issubcata  25846  tartarmap  25888  pgapspf  26052  islocfin  26296  neibastop1  26308  neibastop2lem  26309  neibastop3  26311  topmeet  26313  topjoin  26314  neifg  26320  heibor1lem  26533  heiborlem1  26535  heiborlem8  26542  elrfi  26769  ismrcd1  26773  ismrcd2  26774  istopclsd  26775  mrefg2  26782  isnacs3  26785  pw2f1ocnv  27130  dfac11  27160  islssfg2  27169  filnm  27192  lnr2i  27320  hbtlem6  27333  sdrgacs  27509  stoweidlem57  27806  uslgra1  28118  usgra1  28119  usgraedgrnv  28123  trsspwALT  28592  trsspwALT2  28593  trsspwALT3  28594  pwtrVD  28598  pwtrOLD  28599  pclfinN  30089  lcdlss  31809  mapd1o  31838
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-v 2790  df-in 3159  df-ss 3166  df-pw 3627
  Copyright terms: Public domain W3C validator