Theorem elpw2g 5345

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 4610	. 2 ⊢ (𝐴 ∈ 𝒫 𝐵 → 𝐴 ⊆ 𝐵)
2		ssexg 5324	. . . 4 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → 𝐴 ∈ V)
3		elpwg 4606	. . . . 5 ⊢ (𝐴 ∈ V → (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵))
4	3	biimparc 481	. . . 4 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐴 ∈ V) → 𝐴 ∈ 𝒫 𝐵)
5	2, 4	syldan 592	. . 3 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → 𝐴 ∈ 𝒫 𝐵)
6	5	expcom 415	. 2 ⊢ (𝐵 ∈ 𝑉 → (𝐴 ⊆ 𝐵 → 𝐴 ∈ 𝒫 𝐵))
7	1, 6	impbid2 225	1 ⊢ (𝐵 ∈ 𝑉 → (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵))

Syntax hints:   → wi 4   ↔ wb 205   ∈ wcel 2107  Vcvv 3475   ⊆ wss 3949  𝒫 cpw 4603

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-sep 5300

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477  df-in 3956  df-ss 3966  df-pw 4605

This theorem is referenced by:  elpw2  5346  elpwi2OLD  5348  pwnss  5350  difelpw  5352  rabelpw  5353  pw2f1olem  9076  fineqvlem  9262  elfir  9410  r1sscl  9780  tskwe  9945  dfac8alem  10024  acni2  10041  fin1ai  10288  fin2i  10290  fin23lem7  10311  fin23lem11  10312  isfin2-2  10314  fin23lem39  10345  isf34lem1  10367  isf34lem2  10368  isf34lem4  10372  isf34lem5  10373  fin1a2lem12  10406  canthnumlem  10643  tsken  10749  tskss  10753  gruss  10791  ismre  17534  mreintcl  17539  mremre  17548  submre  17549  mrcval  17554  mrccl  17555  mrcun  17566  ismri  17575  acsfiel  17598  isacs1i  17601  catcoppccl  18067  catcoppcclOLD  18068  acsdrsel  18496  acsdrscl  18499  acsficl  18500  pmtrval  19319  pmtrrn  19325  istopg  22397  uniopn  22399  iscld  22531  ntrval  22540  clsval  22541  discld  22593  mretopd  22596  neival  22606  isnei  22607  lpval  22643  restdis  22682  ordtbaslem  22692  ordtuni  22694  cndis  22795  tgcmp  22905  hauscmplem  22910  comppfsc  23036  elkgen  23040  xkoopn  23093  elqtop  23201  kqffn  23229  isfbas  23333  filss  23357  snfbas  23370  elfg  23375  ufilss  23409  fixufil  23426  cfinufil  23432  ufinffr  23433  ufilen  23434  fin1aufil  23436  flimclslem  23488  hauspwpwf1  23491  supnfcls  23524  flimfnfcls  23532  ptcmplem1  23556  tsmsfbas  23632  blfvalps  23889  blfps  23912  blf  23913  bcthlem5  24845  minveclem3b  24945  sigaclcuni  33116  sigaclcu2  33118  pwsiga  33128  erdsze2lem2  34195  cvmsval  34257  cvmsss2  34265  neibastop2lem  35245  tailf  35260  pibt2  36298  fin2so  36475  sdclem1  36611  elrfirn  41433  elrfirn2  41434  istopclsd  41438  nacsfix  41450  dnnumch1  41786  inpw  47503