Theorem elpw2g 5302

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 4567	. 2 ⊢ (𝐴 ∈ 𝒫 𝐵 → 𝐴 ⊆ 𝐵)
2		ssexg 5288	. . . 4 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → 𝐴 ∈ V)
3		elpwg 4563	. . . . 5 ⊢ (𝐴 ∈ V → (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵))
4	3	biimparc 485	. . . 4 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐴 ∈ V) → 𝐴 ∈ 𝒫 𝐵)
5	2, 4	syldan 603	. . 3 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → 𝐴 ∈ 𝒫 𝐵)
6	5	expcom 419	. 2 ⊢ (𝐵 ∈ 𝑉 → (𝐴 ⊆ 𝐵 → 𝐴 ∈ 𝒫 𝐵))
7	1, 6	impbid2 229	1 ⊢ (𝐵 ∈ 𝑉 → (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∈ wcel 2145  Vcvv 3453   ⊆ wss 3902  𝒫 cpw 4560

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734  ax-sep 5255

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3415  df-v 3455  df-in 3909  df-ss 3919  df-pw 4562

This theorem is used by:  elpw2  5303  rabelpw  5305  difelpw  5322  pw2f1olem  9082  fineqvlem  9239  elfir  9388  r1sscl  9770  tskwe  9958  dfac8alem  10035  acni2  10052  fin1ai  10298  fin2i  10300  fin23lem7  10321  fin23lem11  10322  isfin2-2  10324  fin23lem39  10355  isf34lem1  10377  isf34lem2  10378  isf34lem4  10382  isf34lem5  10383  fin1a2lem12  10416  canthnumlem  10660  tsken  10766  tskss  10770  gruss  10808  ismre  17678  mreintcl  17683  mremre  17692  submre  17693  mrcval  17702  mrccl  17703  mrcun  17714  ismri  17723  acsfiel  17746  isacs1i  17749  catcoppccl  18210  acsdrsel  18635  acsdrscl  18638  acsficl  18639  pmtrval  19582  pmtrrn  19588  istopg  23124  uniopn  23126  iscld  23256  ntrval  23265  clsval  23266  discld  23318  mretopd  23321  neival  23331  isnei  23332  lpval  23368  restdis  23407  ordtbaslem  23417  ordtuni  23419  cndis  23520  tgcmp  23630  hauscmplem  23635  comppfsc  23762  elkgen  23766  xkoopn  23819  elqtop  23927  kqffn  23955  isfbas  24059  filss  24083  snfbas  24096  elfg  24101  ufilss  24135  fixufil  24152  cfinufil  24158  ufinffr  24159  ufilen  24160  fin1aufil  24162  flimclslem  24214  hauspwpwf1  24217  supnfcls  24250  flimfnfcls  24258  ptcmplem1  24282  tsmsfbas  24358  blfvalps  24613  blfps  24636  blf  24637  bcthlem5  25560  minveclem3b  25660  sigaclcuni  34630  sigaclcu2  34632  pwsiga  34642  erdsze2lem2  35785  cvmsval  35847  cvmsss2  35855  neibastop2lem  36981  tailf  36996  pibt2  38173  fin2so  38363  sdclem1  38495  elrfirn  43542  elrfirn2  43543  istopclsd  43547  nacsfix  43559  dnnumch1  43887  inpw  49755