Theorem elpwi 4508

Description: Subset relation implied by membership in a power class. (Contributed by NM, 17-Feb-2007.)

Assertion

Ref	Expression
elpwi	⊢ (𝐴 ∈ 𝒫 𝐵 → 𝐴 ⊆ 𝐵)

Proof of Theorem elpwi

Step	Hyp	Ref	Expression
1		elpwg 4502	. 2 ⊢ (𝐴 ∈ 𝒫 𝐵 → (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵))
2	1	ibi 270	1 ⊢ (𝐴 ∈ 𝒫 𝐵 → 𝐴 ⊆ 𝐵)

Syntax hints:   → wi 4   ∈ wcel 2112   ⊆ wss 3853  𝒫 cpw 4499

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1546  df-ex 1788  df-sb 2073  df-clab 2715  df-cleq 2728  df-clel 2809  df-v 3400  df-in 3860  df-ss 3870  df-pw 4501

This theorem is referenced by:  elpwid  4510  elelpwi  4511  elpwunsn  4585  elpw2g  5222  f1opw2  7438  eldifpw  7531  pwuncl  7533  iunpw  7534  f1opwfi  8958  fi0  9014  marypha1lem  9027  marypha1  9028  marypha2  9033  brwdom2  9167  brwdom3  9176  r1pwss  9365  rankpwi  9404  acndom  9630  acnnum  9631  dfac12r  9725  ackbij2lem1  9798  ackbij1lem6  9804  ackbij1b  9818  isfin2-2  9898  ssfin2  9899  enfin2i  9900  compsscnvlem  9949  compssiso  9953  fin11a  9962  enfin1ai  9963  fin12  9992  fin1a2s  9993  fin1a2  9994  hsmexlem2  10006  tskwe2  10352  inttsk  10353  inatsk  10357  hashbclem  13981  pr2pwpr  14010  elss2prb  14018  qshash  15354  incexclem  15363  incexc  15364  incexc2  15365  rpnnen2lem12  15749  smupf  16000  ramval  16524  ramlb  16535  mrcflem  17063  isacs2  17110  mreacs  17115  acsfn  17116  acsfn1  17118  acsfn2  17120  sscpwex  17274  isacs3lem  18002  isacs4lem  18004  isacs5lem  18005  isacs5  18008  pmtrfrn  18804  oppglsm  18985  acsfn1p  19797  lspf  19965  pptbas  21859  clsf  21899  mretopd  21943  neiptopuni  21981  cncls2  22124  cncls  22125  cnntr  22126  restcnrm  22213  cncmp  22243  tgcmp  22252  uncmp  22254  sscmp  22256  hauscmplem  22257  cmpfi  22259  1stcrest  22304  dis2ndc  22311  lly1stc  22347  dislly  22348  comppfsc  22383  kgentopon  22389  kgen2ss  22406  kgencn  22407  kgencn2  22408  kgencn3  22409  txcmplem2  22493  txcmp  22494  tx1stc  22501  txkgen  22503  xkopt  22506  xkococnlem  22510  xkococn  22511  kqnrmlem1  22594  kqnrmlem2  22595  hmphdis  22647  isfil2  22707  isfild  22709  fbasfip  22719  neifil  22731  trfil2  22738  trufil  22761  fixufil  22773  cfinufil  22779  fin1aufil  22783  fclscmp  22881  alexsubALTlem2  22899  alexsubALTlem3  22900  alexsubALTlem4  22901  ptcmplem5  22907  tgpconncompeqg  22963  imasf1oxms  23341  met2ndc  23375  zdis  23667  icccmp  23676  ovolf  24333  ismbl2  24378  cmmbl  24385  nulmbl  24386  nulmbl2  24387  unmbl  24388  shftmbl  24389  voliunlem2  24402  ioombl1  24413  uniioombl  24440  sqff1o  26018  musum  26027  eengtrkg  27031  edgssv2  27240  upgrreslem  27346  umgrreslem  27347  umgrres1lem  27352  upgrres1  27355  uhgrvd00  27576  rabfodom  30524  elpwincl1  30547  fpwrelmap  30742  cmpcref  31468  pcmplfinf  31479  zarclsint  31490  zarcls  31492  esumcst  31697  esumfsup  31704  esum2d  31727  dmvlsiga  31763  pwsiga  31764  sigaclci  31766  sigainb  31770  insiga  31771  pwldsys  31791  ldgenpisyslem1  31797  ldgenpisyslem3  31799  measinb  31855  measres  31856  cntmeas  31860  volmeas  31865  ddemeas  31870  dya2iocucvr  31917  sxbrsigalem1  31918  omscl  31928  omsf  31929  omsmon  31931  baselcarsg  31939  difelcarsg  31943  carsgsiga  31955  omsmeas  31956  coinflippv  32116  kur14  32845  connpconn  32864  cvmsi  32894  nulsslt  33677  nulssgt  33678  madessno  33730  oldssno  33731  newssno  33732  madebdayim  33756  neibastop1  34234  neibastop2lem  34235  neibastop3  34237  onsucsuccmpi  34318  limsucncmpi  34320  bj-elpwg  34911  bj-0int  34956  bj-ismooredr  34964  lindsdom  35457  ismblfin  35504  cover2  35558  sstotbnd3  35620  heibor1  35654  heibor  35665  pclvalN  37590  pclfinN  37600  pclcmpatN  37601  dochfN  39056  elrfi  40160  cmpfiiin  40163  ismrcd2  40165  isnacs3  40176  aomclem2  40524  islssfg  40539  lmhmfgsplit  40555  lnrfg  40588  rfovcnvf1od  41230  dssmapnvod  41246  neik0pk1imk0  41275  isotone2  41277  ntrclsneine0lem  41292  ntrclsiso  41295  ntrclsk2  41296  ntrclskb  41297  ntrclsk3  41298  ntrclsk13  41299  ntrclsk4  41300  ntrneix2  41321  ntrneik13  41326  ntrrn  41350  dssmapntrcls  41356  ismnushort  41533  sspwtr  42055  sspwtrALT  42056  sspwtrALT2  42057  pwtrVD  42058  pwtrrVD  42059  sspwimp  42152  sspwimpVD  42153  sspwimpcf  42154  sspwimpcfVD  42155  sspwimpALT  42159  sspwimpALT2  42162  pwssfi  42207  ssnnf1octb  42347  dvdmsscn  43095  dvnmptconst  43100  dvnxpaek  43101  dvnmul  43102  dvnprodlem3  43107  ismbl3  43145  ismbl4  43152  stoweidlem57  43216  pwsal  43474  prsal  43477  intsal  43487  salexct  43491  issalnnd  43502  sge0rnre  43520  sge0tsms  43536  sge0cl  43537  sge0fsum  43543  sge0sup  43547  sge0less  43548  sge0gerp  43551  sge0resplit  43562  sge0split  43565  nnfoctbdj  43612  ismeannd  43623  psmeasure  43627  caragen0  43662  caragenunidm  43664  caragenuncl  43669  caragendifcl  43670  omeiunle  43673  carageniuncl  43679  caragensal  43681  caratheodorylem2  43683  0ome  43685  isomennd  43687  caragenel2d  43688  caragencmpl  43691  ovnf  43719  ovn02  43724  ovnsubaddlem1  43726  ovnsubaddlem2  43727  ovnsubadd  43728  hspmbl  43785  isvonmbl  43794  vonmblss2  43798  ovnsubadd2lem  43801  vonvolmbl  43817  nsssmfmbf  43929  smfresal  43937  smfpimbor1lem2  43948  sprsymrelfv  44562  prpair  44569  isomuspgrlem2c  44898  lincdifsn  45381  lcosslsp  45395  lindslinindsimp1  45414  lincresunit3lem1  45436  lincresunit3lem2  45437  lincresunit3  45438  isclatd  45885  elpglem1  46030  aacllem  46119