Theorem elpw2g 5280

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

Syntax hints:   → wi 4   ↔ wb 206   ∈ wcel 2114  Vcvv 3442   ⊆ wss 3903  𝒫 cpw 4556

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5243

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1089  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3402  df-v 3444  df-in 3910  df-ss 3920  df-pw 4558

This theorem is referenced by:  elpw2  5281  rabelpw  5283  difelpw  5301  pw2f1olem  9021  fineqvlem  9178  elfir  9330  r1sscl  9709  tskwe  9874  dfac8alem  9951  acni2  9968  fin1ai  10215  fin2i  10217  fin23lem7  10238  fin23lem11  10239  isfin2-2  10241  fin23lem39  10272  isf34lem1  10294  isf34lem2  10295  isf34lem4  10299  isf34lem5  10300  fin1a2lem12  10333  canthnumlem  10571  tsken  10677  tskss  10681  gruss  10719  ismre  17521  mreintcl  17526  mremre  17535  submre  17536  mrcval  17545  mrccl  17546  mrcun  17557  ismri  17566  acsfiel  17589  isacs1i  17592  catcoppccl  18053  acsdrsel  18478  acsdrscl  18481  acsficl  18482  pmtrval  19392  pmtrrn  19398  istopg  22851  uniopn  22853  iscld  22983  ntrval  22992  clsval  22993  discld  23045  mretopd  23048  neival  23058  isnei  23059  lpval  23095  restdis  23134  ordtbaslem  23144  ordtuni  23146  cndis  23247  tgcmp  23357  hauscmplem  23362  comppfsc  23488  elkgen  23492  xkoopn  23545  elqtop  23653  kqffn  23681  isfbas  23785  filss  23809  snfbas  23822  elfg  23827  ufilss  23861  fixufil  23878  cfinufil  23884  ufinffr  23885  ufilen  23886  fin1aufil  23888  flimclslem  23940  hauspwpwf1  23943  supnfcls  23976  flimfnfcls  23984  ptcmplem1  24008  tsmsfbas  24084  blfvalps  24339  blfps  24362  blf  24363  bcthlem5  25296  minveclem3b  25396  sigaclcuni  34295  sigaclcu2  34297  pwsiga  34307  erdsze2lem2  35417  cvmsval  35479  cvmsss2  35487  neibastop2lem  36573  tailf  36588  pibt2  37661  fin2so  37847  sdclem1  37983  elrfirn  43041  elrfirn2  43042  istopclsd  43046  nacsfix  43058  dnnumch1  43390  inpw  49173