Theorem elpw2g 5278

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 4561	. 2 ⊢ (𝐴 ∈ 𝒫 𝐵 → 𝐴 ⊆ 𝐵)
2		ssexg 5268	. . . 4 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → 𝐴 ∈ V)
3		elpwg 4557	. . . . 5 ⊢ (𝐴 ∈ V → (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵))
4	3	biimparc 479	. . . 4 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐴 ∈ V) → 𝐴 ∈ 𝒫 𝐵)
5	2, 4	syldan 591	. . 3 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → 𝐴 ∈ 𝒫 𝐵)
6	5	expcom 413	. 2 ⊢ (𝐵 ∈ 𝑉 → (𝐴 ⊆ 𝐵 → 𝐴 ∈ 𝒫 𝐵))
7	1, 6	impbid2 226	1 ⊢ (𝐵 ∈ 𝑉 → (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵))

Syntax hints:   → wi 4   ↔ wb 206   ∈ wcel 2113  Vcvv 3440   ⊆ wss 3901  𝒫 cpw 4554

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 2115  ax-9 2123  ax-ext 2708  ax-sep 5241

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3400  df-v 3442  df-in 3908  df-ss 3918  df-pw 4556

This theorem is referenced by:  elpw2  5279  rabelpw  5281  difelpw  5299  pw2f1olem  9009  fineqvlem  9166  elfir  9318  r1sscl  9697  tskwe  9862  dfac8alem  9939  acni2  9956  fin1ai  10203  fin2i  10205  fin23lem7  10226  fin23lem11  10227  isfin2-2  10229  fin23lem39  10260  isf34lem1  10282  isf34lem2  10283  isf34lem4  10287  isf34lem5  10288  fin1a2lem12  10321  canthnumlem  10559  tsken  10665  tskss  10669  gruss  10707  ismre  17509  mreintcl  17514  mremre  17523  submre  17524  mrcval  17533  mrccl  17534  mrcun  17545  ismri  17554  acsfiel  17577  isacs1i  17580  catcoppccl  18041  acsdrsel  18466  acsdrscl  18469  acsficl  18470  pmtrval  19380  pmtrrn  19386  istopg  22839  uniopn  22841  iscld  22971  ntrval  22980  clsval  22981  discld  23033  mretopd  23036  neival  23046  isnei  23047  lpval  23083  restdis  23122  ordtbaslem  23132  ordtuni  23134  cndis  23235  tgcmp  23345  hauscmplem  23350  comppfsc  23476  elkgen  23480  xkoopn  23533  elqtop  23641  kqffn  23669  isfbas  23773  filss  23797  snfbas  23810  elfg  23815  ufilss  23849  fixufil  23866  cfinufil  23872  ufinffr  23873  ufilen  23874  fin1aufil  23876  flimclslem  23928  hauspwpwf1  23931  supnfcls  23964  flimfnfcls  23972  ptcmplem1  23996  tsmsfbas  24072  blfvalps  24327  blfps  24350  blf  24351  bcthlem5  25284  minveclem3b  25384  sigaclcuni  34275  sigaclcu2  34277  pwsiga  34287  erdsze2lem2  35398  cvmsval  35460  cvmsss2  35468  neibastop2lem  36554  tailf  36569  pibt2  37622  fin2so  37808  sdclem1  37944  elrfirn  42937  elrfirn2  42938  istopclsd  42942  nacsfix  42954  dnnumch1  43286  inpw  49070