Theorem elpw2g 5131

Description: Membership in a power class. Theorem 86 of [Suppes] p. 47. (Contributed by NM, 7-Aug-2000.)

Assertion

Ref	Expression
elpw2g	⊢ (𝐵 ∈ 𝑉 → (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵))

Proof of Theorem elpw2g

Step	Hyp	Ref	Expression
1		elpwi 4457	. 2 ⊢ (𝐴 ∈ 𝒫 𝐵 → 𝐴 ⊆ 𝐵)
2		ssexg 5111	. . . 4 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → 𝐴 ∈ V)
3		elpwg 4455	. . . . 5 ⊢ (𝐴 ∈ V → (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵))
4	3	biimparc 480	. . . 4 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐴 ∈ V) → 𝐴 ∈ 𝒫 𝐵)
5	2, 4	syldan 591	. . 3 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → 𝐴 ∈ 𝒫 𝐵)
6	5	expcom 414	. 2 ⊢ (𝐵 ∈ 𝑉 → (𝐴 ⊆ 𝐵 → 𝐴 ∈ 𝒫 𝐵))
7	1, 6	impbid2 227	1 ⊢ (𝐵 ∈ 𝑉 → (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵))

Syntax hints:   → wi 4   ↔ wb 207   ∈ wcel 2079  Vcvv 3432   ⊆ wss 3854  𝒫 cpw 4447

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1775  ax-4 1789  ax-5 1886  ax-6 1945  ax-7 1990  ax-8 2081  ax-9 2089  ax-10 2110  ax-11 2124  ax-12 2139  ax-ext 2767  ax-sep 5088

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-tru 1523  df-ex 1760  df-nf 1764  df-sb 2041  df-clab 2774  df-cleq 2786  df-clel 2861  df-nfc 2933  df-v 3434  df-in 3861  df-ss 3869  df-pw 4449

This theorem is referenced by:  elpw2  5132  elpwi2  5133  pwnss  5134  difelpw  5136  rabelpw  5137  pw2f1olem  8458  fineqvlem  8568  elfir  8715  r1sscl  9049  tskwe  9214  dfac8alem  9290  acni2  9307  fin1ai  9550  fin2i  9552  fin23lem7  9573  fin23lem11  9574  isfin2-2  9576  fin23lem39  9607  isf34lem1  9629  isf34lem2  9630  isf34lem4  9634  isf34lem5  9635  fin1a2lem12  9668  canthnumlem  9905  tsken  10011  tskss  10015  gruss  10053  ismre  16678  mreintcl  16683  mremre  16692  submre  16693  mrcval  16698  mrccl  16699  mrcun  16710  ismri  16719  acsfiel  16742  isacs1i  16745  catcoppccl  17185  acsdrsel  17594  acsdrscl  17597  acsficl  17598  pmtrval  18298  pmtrrn  18304  istopg  21175  uniopn  21177  iscld  21307  ntrval  21316  clsval  21317  discld  21369  mretopd  21372  neival  21382  isnei  21383  lpval  21419  restdis  21458  ordtbaslem  21468  ordtuni  21470  cndis  21571  tgcmp  21681  hauscmplem  21686  comppfsc  21812  elkgen  21816  xkoopn  21869  elqtop  21977  kqffn  22005  isfbas  22109  filss  22133  snfbas  22146  elfg  22151  ufilss  22185  fixufil  22202  cfinufil  22208  ufinffr  22209  ufilen  22210  fin1aufil  22212  flimclslem  22264  hauspwpwf1  22267  supnfcls  22300  flimfnfcls  22308  ptcmplem1  22332  tsmsfbas  22407  blfvalps  22664  blfps  22687  blf  22688  bcthlem5  23602  minveclem3b  23702  sigaclcuni  30950  sigaclcu2  30952  pwsiga  30962  erdsze2lem2  32015  cvmsval  32077  cvmsss2  32085  neibastop2lem  33262  tailf  33277  bj-ismoored  33945  pibt2  34175  fin2so  34356  sdclem1  34496  elrfirn  38727  elrfirn2  38728  istopclsd  38732  nacsfix  38744  dnnumch1  39080