Theorem elpwi 4557

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

Syntax hints:   → wi 4   ∈ wcel 2111   ⊆ wss 3902  𝒫 cpw 4550

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-ss 3919  df-pw 4552

This theorem is referenced by:  elpwid  4559  elelpwi  4560  elpwunsn  4637  elpw2g  5271  f1opw2  7601  eldifpw  7701  pwuncl  7703  iunpw  7704  mptcnfimad  7918  pwssfi  9086  f1opwfi  9240  fi0  9304  marypha1lem  9317  marypha1  9318  marypha2  9323  brwdom2  9459  brwdom3  9468  r1pwss  9674  rankpwi  9713  acndom  9939  acnnum  9940  dfac12r  10035  ackbij2lem1  10106  ackbij1lem6  10112  ackbij1b  10126  isfin2-2  10207  ssfin2  10208  enfin2i  10209  compsscnvlem  10258  compssiso  10262  fin11a  10271  enfin1ai  10272  fin12  10301  fin1a2s  10302  fin1a2  10303  hsmexlem2  10315  tskwe2  10661  inttsk  10662  inatsk  10666  hashbclem  14356  pr2pwpr  14383  elss2prb  14392  qshash  15731  incexclem  15740  incexc  15741  incexc2  15742  rpnnen2lem12  16131  smupf  16386  ramval  16917  ramlb  16928  mrcflem  17509  isacs2  17556  mreacs  17561  acsfn  17562  acsfn1  17564  acsfn2  17566  sscpwex  17719  isacs3lem  18445  isacs4lem  18447  isacs5lem  18448  isacs5  18451  pmtrfrn  19368  oppglsm  19552  acsfn1p  20712  lspf  20905  pptbas  22921  clsf  22961  mretopd  23005  neiptopuni  23043  cncls2  23186  cncls  23187  cnntr  23188  restcnrm  23275  cncmp  23305  tgcmp  23314  uncmp  23316  sscmp  23318  hauscmplem  23319  cmpfi  23321  1stcrest  23366  dis2ndc  23373  lly1stc  23409  dislly  23410  comppfsc  23445  kgentopon  23451  kgen2ss  23468  kgencn  23469  kgencn2  23470  kgencn3  23471  txcmplem2  23555  txcmp  23556  tx1stc  23563  txkgen  23565  xkopt  23568  xkococnlem  23572  xkococn  23573  kqnrmlem1  23656  kqnrmlem2  23657  hmphdis  23709  isfil2  23769  isfild  23771  fbasfip  23781  neifil  23793  trfil2  23800  trufil  23823  fixufil  23835  cfinufil  23841  fin1aufil  23845  fclscmp  23943  alexsubALTlem2  23961  alexsubALTlem3  23962  alexsubALTlem4  23963  ptcmplem5  23969  tgpconncompeqg  24025  imasf1oxms  24402  met2ndc  24436  zdis  24730  icccmp  24739  ovolf  25408  ismbl2  25453  cmmbl  25460  nulmbl  25461  nulmbl2  25462  unmbl  25463  shftmbl  25464  voliunlem2  25477  ioombl1  25488  uniioombl  25515  sqff1o  27117  musum  27126  nulsslt  27736  nulssgt  27737  madessno  27799  oldssno  27800  newssno  27801  madebdayim  27831  eengtrkg  28962  edgssv2  29174  upgrreslem  29280  umgrreslem  29281  umgrres1lem  29286  upgrres1  29289  uhgrvd00  29511  rabfodom  32480  elpwincl1  32500  fpwrelmap  32711  cmpcref  33858  pcmplfinf  33869  zarclsint  33880  zarcls  33882  esumcst  34071  esumfsup  34078  esum2d  34101  dmvlsiga  34137  pwsiga  34138  sigaclci  34140  sigainb  34144  insiga  34145  pwldsys  34165  ldgenpisyslem1  34171  ldgenpisyslem3  34173  measinb  34229  measres  34230  cntmeas  34234  volmeas  34239  ddemeas  34244  dya2iocucvr  34292  sxbrsigalem1  34293  omscl  34303  omsf  34304  omsmon  34306  baselcarsg  34314  difelcarsg  34318  carsgsiga  34330  omsmeas  34331  coinflippv  34492  kur14  35248  connpconn  35267  cvmsi  35297  neibastop1  36392  neibastop2lem  36393  neibastop3  36395  onsucsuccmpi  36476  limsucncmpi  36478  bj-elpwg  37085  bj-0int  37134  bj-ismooredr  37142  lindsdom  37653  ismblfin  37700  cover2  37754  sstotbnd3  37815  heibor1  37849  heibor  37860  pclvalN  39928  pclfinN  39938  pclcmpatN  39939  dochfN  41394  elrfi  42726  cmpfiiin  42729  ismrcd2  42731  isnacs3  42742  aomclem2  43087  islssfg  43102  lmhmfgsplit  43118  lnrfg  43151  dfno2  43460  rfovcnvf1od  44036  dssmapnvod  44052  neik0pk1imk0  44079  isotone2  44081  ntrclsneine0lem  44096  ntrclsiso  44099  ntrclsk2  44100  ntrclskb  44101  ntrclsk3  44102  ntrclsk13  44103  ntrclsk4  44104  ntrneix2  44125  ntrneik13  44130  ntrrn  44154  dssmapntrcls  44160  ismnushort  44333  sspwtr  44852  sspwtrALT  44853  sspwtrALT2  44854  pwtrVD  44855  pwtrrVD  44856  sspwimp  44949  sspwimpVD  44950  sspwimpcf  44951  sspwimpcfVD  44952  sspwimpALT  44956  sspwimpALT2  44959  ssnnf1octb  45230  dvdmsscn  45973  dvnmptconst  45978  dvnxpaek  45979  dvnmul  45980  dvnprodlem3  45985  ismbl3  46023  ismbl4  46030  stoweidlem57  46094  pwsal  46352  prsal  46355  intsal  46367  salexct  46371  issalnnd  46382  sge0rnre  46401  sge0tsms  46417  sge0cl  46418  sge0fsum  46424  sge0sup  46428  sge0less  46429  sge0gerp  46432  sge0resplit  46443  sge0split  46446  nnfoctbdj  46493  ismeannd  46504  psmeasure  46508  caragen0  46543  caragenunidm  46545  caragenuncl  46550  caragendifcl  46551  omeiunle  46554  carageniuncl  46560  caragensal  46562  caratheodorylem2  46564  0ome  46566  isomennd  46568  caragenel2d  46569  caragencmpl  46572  ovnf  46600  ovn02  46605  ovnsubaddlem1  46607  ovnsubaddlem2  46608  ovnsubadd  46609  hspmbl  46666  isvonmbl  46675  vonmblss2  46679  ovnsubadd2lem  46682  vonvolmbl  46698  nsssmfmbf  46816  smfresal  46825  smfpimbor1lem2  46836  sprsymrelfv  47524  prpair  47531  grtriprop  47971  lincdifsn  48455  lcosslsp  48469  lindslinindsimp1  48488  lincresunit3lem1  48510  lincresunit3lem2  48511  lincresunit3  48512  isclatd  49013  elpglem1  49742  aacllem  49832