Theorem elpw2g 5275

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 4549	. 2 ⊢ (𝐴 ∈ 𝒫 𝐵 → 𝐴 ⊆ 𝐵)
2		ssexg 5265	. . . 4 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → 𝐴 ∈ V)
3		elpwg 4545	. . . . 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 3430   ⊆ wss 3890  𝒫 cpw 4542

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 5232

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 3391  df-v 3432  df-in 3897  df-ss 3907  df-pw 4544

This theorem is referenced by:  elpw2  5276  rabelpw  5278  difelpw  5296  pw2f1olem  9019  fineqvlem  9176  elfir  9328  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  17552  mreintcl  17557  mremre  17566  submre  17567  mrcval  17576  mrccl  17577  mrcun  17588  ismri  17597  acsfiel  17620  isacs1i  17623  catcoppccl  18084  acsdrsel  18509  acsdrscl  18512  acsficl  18513  pmtrval  19426  pmtrrn  19432  istopg  22860  uniopn  22862  iscld  22992  ntrval  23001  clsval  23002  discld  23054  mretopd  23057  neival  23067  isnei  23068  lpval  23104  restdis  23143  ordtbaslem  23153  ordtuni  23155  cndis  23256  tgcmp  23366  hauscmplem  23371  comppfsc  23497  elkgen  23501  xkoopn  23554  elqtop  23662  kqffn  23690  isfbas  23794  filss  23818  snfbas  23831  elfg  23836  ufilss  23870  fixufil  23887  cfinufil  23893  ufinffr  23894  ufilen  23895  fin1aufil  23897  flimclslem  23949  hauspwpwf1  23952  supnfcls  23985  flimfnfcls  23993  ptcmplem1  24017  tsmsfbas  24093  blfvalps  24348  blfps  24371  blf  24372  bcthlem5  25295  minveclem3b  25395  sigaclcuni  34262  sigaclcu2  34264  pwsiga  34274  erdsze2lem2  35386  cvmsval  35448  cvmsss2  35456  neibastop2lem  36542  tailf  36557  pibt2  37733  fin2so  37928  sdclem1  38064  elrfirn  43127  elrfirn2  43128  istopclsd  43132  nacsfix  43144  dnnumch1  43472  inpw  49294