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

Theorem elpwi 4201
Description: Subset relation implied by membership in a power class. (Contributed by NM, 17-Feb-2007.)
Assertion
Ref Expression
elpwi (𝐴 ∈ 𝒫 𝐵𝐴𝐵)

Proof of Theorem elpwi
StepHypRef Expression
1 elpwg 4199 . 2 (𝐴 ∈ 𝒫 𝐵 → (𝐴 ∈ 𝒫 𝐵𝐴𝐵))
21ibi 256 1 (𝐴 ∈ 𝒫 𝐵𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2030  wss 3607  𝒫 cpw 4191
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-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-v 3233  df-in 3614  df-ss 3621  df-pw 4193
This theorem is referenced by:  elpwid  4203  elelpwi  4204  elpwunsn  4256  elpw2g  4857  f1opw2  6930  eldifpw  7018  iunpw  7020  f1opwfi  8311  fi0  8367  fiin  8369  marypha1lem  8380  marypha1  8381  marypha2  8386  brwdom2  8519  brwdom3  8528  r1pwss  8685  rankpwi  8724  acndom  8912  acnnum  8913  dfac12r  9006  ackbij2lem1  9079  ackbij1lem6  9085  ackbij1b  9099  isfin2-2  9179  ssfin2  9180  enfin2i  9181  compsscnvlem  9230  compssiso  9234  fin11a  9243  enfin1ai  9244  fin12  9273  fin1a2s  9274  fin1a2  9275  hsmexlem2  9287  tskwe2  9633  inttsk  9634  inatsk  9638  hashbclem  13274  pr2pwpr  13299  elss2prb  13307  qshash  14603  incexclem  14612  incexc  14613  incexc2  14614  rpnnen2lem12  14998  smupf  15247  ramval  15759  ramlb  15770  mrcflem  16313  isacs2  16361  mreacs  16366  acsfn  16367  acsfn1  16369  acsfn2  16371  sscpwex  16522  fpwipodrs  17211  isacs3lem  17213  isacs4lem  17215  isacs5lem  17216  isacs5  17219  pmtrfrn  17924  oppglsm  18103  lspf  19022  pptbas  20860  clsf  20900  mretopd  20944  neiptopuni  20982  cncls2  21125  cncls  21126  cnntr  21127  restcnrm  21214  cncmp  21243  tgcmp  21252  uncmp  21254  sscmp  21256  hauscmplem  21257  cmpfi  21259  1stcrest  21304  dis2ndc  21311  lly1stc  21347  dislly  21348  comppfsc  21383  kgentopon  21389  kgen2ss  21406  kgencn  21407  kgencn2  21408  kgencn3  21409  txcmplem2  21493  txcmp  21494  tx1stc  21501  txkgen  21503  xkopt  21506  xkococnlem  21510  xkococn  21511  kqnrmlem1  21594  kqnrmlem2  21595  hmphdis  21647  isfil2  21707  isfild  21709  fbasfip  21719  neifil  21731  trfil2  21738  trufil  21761  fixufil  21773  cfinufil  21779  fin1aufil  21783  fclscmp  21881  alexsubALTlem2  21899  alexsubALTlem3  21900  alexsubALTlem4  21901  ptcmplem5  21907  tgpconncompeqg  21962  imasf1oxms  22341  met2ndc  22375  zdis  22666  icccmp  22675  ovolf  23296  ismbl2  23341  cmmbl  23348  nulmbl  23349  nulmbl2  23350  unmbl  23351  shftmbl  23352  voliunlem2  23365  ioombl1  23376  uniioombl  23403  sqff1o  24953  musum  24962  eengtrkg  25910  edgssv2  26135  upgrreslem  26241  umgrreslem  26242  umgrres1lem  26247  upgrres1  26250  uhgrvd00  26486  rabfodom  29470  elpwincl1  29483  fpwrelmap  29636  cmpcref  30045  pcmplfinf  30056  esumcst  30253  esumfsup  30260  esum2d  30283  dmvlsiga  30320  pwsiga  30321  sigaclci  30323  sigainb  30327  insiga  30328  pwldsys  30348  ldgenpisyslem1  30354  ldgenpisyslem3  30356  measinb  30412  measres  30413  cntmeas  30417  volmeas  30422  ddemeas  30427  dya2iocucvr  30474  sxbrsigalem1  30475  omscl  30485  omsf  30486  omsmon  30488  baselcarsg  30496  difelcarsg  30500  carsgsiga  30512  omsmeas  30513  coinflippv  30673  kur14  31324  connpconn  31343  cvmsi  31373  nulsslt  32033  nulssgt  32034  neibastop1  32479  neibastop2lem  32480  neibastop3  32482  onsucsuccmpi  32567  limsucncmpi  32569  bj-0int  33180  bj-ismooredr  33189  lindsdom  33533  ismblfin  33580  cover2  33638  sstotbnd3  33705  heibor1  33739  heibor  33750  pclvalN  35494  pclfinN  35504  pclcmpatN  35505  dochfN  36962  elrfi  37574  cmpfiiin  37577  ismrcd2  37579  isnacs3  37590  aomclem2  37942  islssfg  37957  lmhmfgsplit  37973  lnrfg  38006  acsfn1p  38086  rfovcnvf1od  38615  dssmapnvod  38631  clsk1indlem3  38658  neik0pk1imk0  38662  isotone1  38663  isotone2  38664  ntrclsneine0lem  38679  ntrclsiso  38682  ntrclsk2  38683  ntrclskb  38684  ntrclsk3  38685  ntrclsk13  38686  ntrclsk4  38687  ntrneix2  38708  ntrneik13  38713  ntrrn  38737  dssmapntrcls  38743  sspwtr  39365  sspwtrALT  39366  sspwtrALT2  39372  pwtrVD  39373  pwtrrVD  39374  sspwimp  39468  sspwimpVD  39469  sspwimpcf  39470  sspwimpcfVD  39471  sspwimpALT  39475  sspwimpALT2  39478  pwssfi  39525  ssnnf1octb  39696  dvdmsscn  40469  dvnmptconst  40474  dvnxpaek  40475  dvnmul  40476  dvnprodlem3  40481  ismbl3  40521  ismbl4  40528  stoweidlem57  40592  pwsal  40853  prsal  40856  intsal  40866  salexct  40870  issalnnd  40881  sge0rnre  40899  sge0tsms  40915  sge0cl  40916  sge0fsum  40922  sge0sup  40926  sge0less  40927  sge0gerp  40930  sge0resplit  40941  sge0split  40944  nnfoctbdj  40991  ismeannd  41002  psmeasure  41006  caragen0  41041  caragenunidm  41043  caragenuncl  41048  caragendifcl  41049  omeiunle  41052  carageniuncl  41058  caragensal  41060  caratheodorylem2  41062  0ome  41064  isomennd  41066  caragenel2d  41067  caragencmpl  41070  ovnf  41098  ovn02  41103  ovnsubaddlem1  41105  ovnsubaddlem2  41106  ovnsubadd  41107  hspmbl  41164  isvonmbl  41173  vonmblss2  41177  ovnsubadd2lem  41180  vonvolmbl  41196  nsssmfmbf  41308  smfresal  41316  smfpimbor1lem2  41327  sprsymrelfv  42069  lincdifsn  42538  lcosslsp  42552  lindslinindsimp1  42571  lincresunit3lem1  42593  lincresunit3lem2  42594  lincresunit3  42595  elpglem1  42782  aacllem  42875
  Copyright terms: Public domain W3C validator