Theorem elpw2g 5339

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 4612	. 2 ⊢ (𝐴 ∈ 𝒫 𝐵 → 𝐴 ⊆ 𝐵)
2		ssexg 5329	. . . 4 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → 𝐴 ∈ V)
3		elpwg 4608	. . . . 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 2106  Vcvv 3478   ⊆ wss 3963  𝒫 cpw 4605

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706  ax-sep 5302

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1540  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-rab 3434  df-v 3480  df-in 3970  df-ss 3980  df-pw 4607

This theorem is referenced by:  elpw2  5340  rabelpw  5342  difelpw  5360  pw2f1olem  9115  fineqvlem  9296  elfir  9453  r1sscl  9823  tskwe  9988  dfac8alem  10067  acni2  10084  fin1ai  10331  fin2i  10333  fin23lem7  10354  fin23lem11  10355  isfin2-2  10357  fin23lem39  10388  isf34lem1  10410  isf34lem2  10411  isf34lem4  10415  isf34lem5  10416  fin1a2lem12  10449  canthnumlem  10686  tsken  10792  tskss  10796  gruss  10834  ismre  17635  mreintcl  17640  mremre  17649  submre  17650  mrcval  17655  mrccl  17656  mrcun  17667  ismri  17676  acsfiel  17699  isacs1i  17702  catcoppccl  18171  catcoppcclOLD  18172  acsdrsel  18601  acsdrscl  18604  acsficl  18605  pmtrval  19484  pmtrrn  19490  istopg  22917  uniopn  22919  iscld  23051  ntrval  23060  clsval  23061  discld  23113  mretopd  23116  neival  23126  isnei  23127  lpval  23163  restdis  23202  ordtbaslem  23212  ordtuni  23214  cndis  23315  tgcmp  23425  hauscmplem  23430  comppfsc  23556  elkgen  23560  xkoopn  23613  elqtop  23721  kqffn  23749  isfbas  23853  filss  23877  snfbas  23890  elfg  23895  ufilss  23929  fixufil  23946  cfinufil  23952  ufinffr  23953  ufilen  23954  fin1aufil  23956  flimclslem  24008  hauspwpwf1  24011  supnfcls  24044  flimfnfcls  24052  ptcmplem1  24076  tsmsfbas  24152  blfvalps  24409  blfps  24432  blf  24433  bcthlem5  25376  minveclem3b  25476  sigaclcuni  34099  sigaclcu2  34101  pwsiga  34111  erdsze2lem2  35189  cvmsval  35251  cvmsss2  35259  neibastop2lem  36343  tailf  36358  pibt2  37400  fin2so  37594  sdclem1  37730  elrfirn  42683  elrfirn2  42684  istopclsd  42688  nacsfix  42700  dnnumch1  43033  inpw  48667