Theorem elpw2g 5333

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 4607	. 2 ⊢ (𝐴 ∈ 𝒫 𝐵 → 𝐴 ⊆ 𝐵)
2		ssexg 5323	. . . 4 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → 𝐴 ∈ V)
3		elpwg 4603	. . . . 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 2108  Vcvv 3480   ⊆ wss 3951  𝒫 cpw 4600

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-sep 5296

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1089  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-v 3482  df-in 3958  df-ss 3968  df-pw 4602

This theorem is referenced by:  elpw2  5334  rabelpw  5336  difelpw  5354  pw2f1olem  9116  fineqvlem  9298  elfir  9455  r1sscl  9825  tskwe  9990  dfac8alem  10069  acni2  10086  fin1ai  10333  fin2i  10335  fin23lem7  10356  fin23lem11  10357  isfin2-2  10359  fin23lem39  10390  isf34lem1  10412  isf34lem2  10413  isf34lem4  10417  isf34lem5  10418  fin1a2lem12  10451  canthnumlem  10688  tsken  10794  tskss  10798  gruss  10836  ismre  17633  mreintcl  17638  mremre  17647  submre  17648  mrcval  17653  mrccl  17654  mrcun  17665  ismri  17674  acsfiel  17697  isacs1i  17700  catcoppccl  18162  acsdrsel  18588  acsdrscl  18591  acsficl  18592  pmtrval  19469  pmtrrn  19475  istopg  22901  uniopn  22903  iscld  23035  ntrval  23044  clsval  23045  discld  23097  mretopd  23100  neival  23110  isnei  23111  lpval  23147  restdis  23186  ordtbaslem  23196  ordtuni  23198  cndis  23299  tgcmp  23409  hauscmplem  23414  comppfsc  23540  elkgen  23544  xkoopn  23597  elqtop  23705  kqffn  23733  isfbas  23837  filss  23861  snfbas  23874  elfg  23879  ufilss  23913  fixufil  23930  cfinufil  23936  ufinffr  23937  ufilen  23938  fin1aufil  23940  flimclslem  23992  hauspwpwf1  23995  supnfcls  24028  flimfnfcls  24036  ptcmplem1  24060  tsmsfbas  24136  blfvalps  24393  blfps  24416  blf  24417  bcthlem5  25362  minveclem3b  25462  sigaclcuni  34119  sigaclcu2  34121  pwsiga  34131  erdsze2lem2  35209  cvmsval  35271  cvmsss2  35279  neibastop2lem  36361  tailf  36376  pibt2  37418  fin2so  37614  sdclem1  37750  elrfirn  42706  elrfirn2  42707  istopclsd  42711  nacsfix  42723  dnnumch1  43056  inpw  48738