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  19579  pmtrrn  19585  istopg  23121  uniopn  23123  iscld  23253  ntrval  23262  clsval  23263  discld  23315  mretopd  23318  neival  23328  isnei  23329  lpval  23365  restdis  23404  ordtbaslem  23414  ordtuni  23416  cndis  23517  tgcmp  23627  hauscmplem  23632  comppfsc  23759  elkgen  23763  xkoopn  23816  elqtop  23924  kqffn  23952  isfbas  24056  filss  24080  snfbas  24093  elfg  24098  ufilss  24132  fixufil  24149  cfinufil  24155  ufinffr  24156  ufilen  24157  fin1aufil  24159  flimclslem  24211  hauspwpwf1  24214  supnfcls  24247  flimfnfcls  24255  ptcmplem1  24279  tsmsfbas  24355  blfvalps  24610  blfps  24633  blf  24634  bcthlem5  25557  minveclem3b  25657  sigaclcuni  34615  sigaclcu2  34617  pwsiga  34627  erdsze2lem2  35770  cvmsval  35832  cvmsss2  35840  neibastop2lem  36966  tailf  36981  pibt2  38158  fin2so  38348  sdclem1  38480  elrfirn  43527  elrfirn2  43528  istopclsd  43532  nacsfix  43544  dnnumch1  43872  inpw  49740