Theorem elpwi 4564

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 4560	. 2 ⊢ (𝐴 ∈ 𝒫 𝐵 → (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵))
2	1	ibi 270	1 ⊢ (𝐴 ∈ 𝒫 𝐵 → 𝐴 ⊆ 𝐵)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145   ⊆ wss 3899  𝒫 cpw 4557

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-ss 3916  df-pw 4559

This theorem is used by:  elpwid  4566  elelpwi  4567  elpwunsn  4645  elpw2g  5295  f1opw2  7668  eldifpw  7771  pwuncl  7773  iunpw  7774  mptcnfimad  7987  pwssfi  9176  f1opwfi  9329  fi0  9396  marypha1lem  9409  marypha1  9410  marypha2  9415  brwdom2  9551  brwdom3  9560  r1pwss  9774  rankpwi  9813  acndom  10111  acnnum  10112  dfac12r  10206  ackbij2lem1  10277  ackbij1lem6  10283  ackbij1b  10297  isfin2-2  10378  ssfin2  10379  enfin2i  10380  compsscnvlem  10429  compssiso  10433  fin11a  10442  enfin1ai  10443  fin12  10472  fin1a2s  10473  fin1a2  10474  hsmexlem2  10486  tskwe2  10839  inttsk  10840  inatsk  10844  indval0  12305  hashbclem  14577  pr2pwpr  14604  elss2prb  14613  qshash  15974  incexclem  15985  incexc  15986  incexc2  15987  rpnnen2lem12  16373  smupf  16628  ramval  17166  ramlb  17177  mrcflem  17760  isacs2  17807  mreacs  17812  acsfn  17813  acsfn1  17815  acsfn2  17817  sscpwex  17970  isacs3lem  18696  isacs4lem  18698  isacs5lem  18699  isacs5  18702  pmtrfrn  19652  oppglsm  19836  acsfn1p  21036  lspf  21229  lindsdom  22136  pptbas  23306  clsf  23346  mretopd  23390  neiptopuni  23428  cncls2  23571  cncls  23572  cnntr  23573  restcnrm  23660  cncmp  23690  tgcmp  23699  uncmp  23701  sscmp  23703  hauscmplem  23704  cmpfi  23706  1stcrest  23751  dis2ndc  23759  lly1stc  23795  dislly  23796  comppfsc  23831  kgentopon  23837  kgen2ss  23854  kgencn  23855  kgencn2  23856  kgencn3  23857  txcmplem2  23941  txcmp  23942  tx1stc  23949  txkgen  23951  xkopt  23954  xkococnlem  23958  xkococn  23959  kqnrmlem1  24042  kqnrmlem2  24043  hmphdis  24095  isfil2  24155  isfild  24157  fbasfip  24167  neifil  24179  trfil2  24186  trufil  24209  fixufil  24221  cfinufil  24227  fin1aufil  24231  fclscmp  24329  alexsubALTlem2  24347  alexsubALTlem3  24348  alexsubALTlem4  24349  ptcmplem5  24355  tgpconncompeqg  24411  imasf1oxms  24788  met2ndc  24822  zdis  25116  icccmp  25125  ovolf  25783  ismbl2  25828  cmmbl  25835  nulmbl  25836  nulmbl2  25837  unmbl  25838  shftmbl  25839  voliunlem2  25852  ioombl1  25863  uniioombl  25890  sqff1o  27491  musum  27500  nulslts  28143  nulsgts  28144  madessno  28208  oldssno  28209  newssno  28210  madebdayim  28256  eengtrkg  29546  edgssv2  29761  upgrreslem  29867  umgrreslem  29868  umgrres1lem  29873  upgrres1  29876  uhgrvd00  30097  rabfodom  33083  elpwincl1  33103  fpwrelmap  33307  esplyfval2  34179  cmpcref  34464  pcmplfinf  34475  zarclsint  34486  zarcls  34488  esumcst  34677  esumfsup  34684  esum2d  34707  dmvlsiga  34743  pwsiga  34744  sigaclci  34746  sigainb  34751  insiga  34752  pwldsys  34772  ldgenpisyslem1  34778  ldgenpisyslem3  34780  measinb  34836  measres  34837  cntmeas  34841  volmeas  34846  ddemeas  34851  dya2iocucvr  34899  sxbrsigalem1  34900  omscl  34910  omsf  34911  omsmon  34913  baselcarsg  34921  difelcarsg  34925  carsgsiga  34937  omsmeas  34938  coinflippv  35099  kur14  35950  connpconn  35969  cvmsi  35999  neibastop1  37117  neibastop2lem  37118  neibastop3  37120  onsucsuccmpi  37201  limsucncmpi  37203  bj-elpwg  37935  bj-0int  37990  bj-ismooredr  37998  ismblfin  38547  cover2  38617  sstotbnd3  38678  heibor1  38712  heibor  38723  pclvalN  40915  pclfinN  40925  pclcmpatN  40926  dochfN  42381  elrfi  43658  cmpfiiin  43661  ismrcd2  43663  isnacs3  43674  aomclem2  44015  islssfg  44030  lmhmfgsplit  44046  lnrfg  44079  dfno2  44387  rfovcnvf1od  44963  dssmapnvod  44979  neik0pk1imk0  45006  isotone2  45008  ntrclsneine0lem  45023  ntrclsiso  45026  ntrclsk2  45027  ntrclskb  45028  ntrclsk3  45029  ntrclsk13  45030  ntrclsk4  45031  ntrneix2  45052  ntrneik13  45057  ntrrn  45081  dssmapntrcls  45087  ismnushort  45244  sspwtr  45762  sspwtrALT  45763  sspwtrALT2  45764  pwtrVD  45765  pwtrrVD  45766  sspwimp  45859  sspwimpVD  45860  sspwimpcf  45861  sspwimpcfVD  45862  sspwimpALT  45866  sspwimpALT2  45869  ssnnf1octb  46152  dvdmsscn  46890  dvnmptconst  46895  dvnxpaek  46896  dvnmul  46897  dvnprodlem3  46902  ismbl3  46940  ismbl4  46947  stoweidlem57  47011  pwsal  47269  prsal  47272  intsal  47284  salexct  47288  issalnnd  47299  sge0rnre  47318  sge0tsms  47334  sge0cl  47335  sge0fsum  47341  sge0sup  47345  sge0less  47346  sge0gerp  47349  sge0resplit  47360  sge0split  47363  nnfoctbdj  47410  ismeannd  47421  psmeasure  47425  caragen0  47460  caragenunidm  47462  caragenuncl  47467  caragendifcl  47468  omeiunle  47471  carageniuncl  47477  caragensal  47479  caratheodorylem2  47481  0ome  47483  isomennd  47485  caragenel2d  47486  caragencmpl  47489  ovnf  47517  ovn02  47522  ovnsubaddlem1  47524  ovnsubaddlem2  47525  ovnsubadd  47526  hspmbl  47583  isvonmbl  47592  vonmblss2  47596  ovnsubadd2lem  47599  vonvolmbl  47615  nsssmfmbf  47733  smfresal  47742  smfpimbor1lem2  47753  sprsymrelfv  48520  prpair  48527  grtriprop  48983  lincdifsn  49480  lcosslsp  49494  lindslinindsimp1  49513  lincresunit3lem1  49535  lincresunit3lem2  49536  lincresunit3  49537  isclatd  50035  elpglem1  50748  aacllem  50883