Theorem elpw2g 5268

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 4549	. 2 ⊢ (𝐴 ∈ 𝒫 𝐵 → 𝐴 ⊆ 𝐵)
2		ssexg 5258	. . . 4 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → 𝐴 ∈ V)
3		elpwg 4545	. . . . 5 ⊢ (𝐴 ∈ V → (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵))
4	3	biimparc 479	. . . 4 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐴 ∈ V) → 𝐴 ∈ 𝒫 𝐵)
5	2, 4	syldan 592	. . 3 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → 𝐴 ∈ 𝒫 𝐵)
6	5	expcom 413	. 2 ⊢ (𝐵 ∈ 𝑉 → (𝐴 ⊆ 𝐵 → 𝐴 ∈ 𝒫 𝐵))
7	1, 6	impbid2 226	1 ⊢ (𝐵 ∈ 𝑉 → (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵))

Syntax hints:   → wi 4   ↔ wb 206   ∈ wcel 2114  Vcvv 3430   ⊆ wss 3890  𝒫 cpw 4542

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5231

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1089  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3391  df-v 3432  df-in 3897  df-ss 3907  df-pw 4544

This theorem is referenced by:  elpw2  5269  rabelpw  5271  difelpw  5289  pw2f1olem  9010  fineqvlem  9167  elfir  9319  r1sscl  9698  tskwe  9863  dfac8alem  9940  acni2  9957  fin1ai  10204  fin2i  10206  fin23lem7  10227  fin23lem11  10228  isfin2-2  10230  fin23lem39  10261  isf34lem1  10283  isf34lem2  10284  isf34lem4  10288  isf34lem5  10289  fin1a2lem12  10322  canthnumlem  10560  tsken  10666  tskss  10670  gruss  10708  ismre  17510  mreintcl  17515  mremre  17524  submre  17525  mrcval  17534  mrccl  17535  mrcun  17546  ismri  17555  acsfiel  17578  isacs1i  17581  catcoppccl  18042  acsdrsel  18467  acsdrscl  18470  acsficl  18471  pmtrval  19384  pmtrrn  19390  istopg  22838  uniopn  22840  iscld  22970  ntrval  22979  clsval  22980  discld  23032  mretopd  23035  neival  23045  isnei  23046  lpval  23082  restdis  23121  ordtbaslem  23131  ordtuni  23133  cndis  23234  tgcmp  23344  hauscmplem  23349  comppfsc  23475  elkgen  23479  xkoopn  23532  elqtop  23640  kqffn  23668  isfbas  23772  filss  23796  snfbas  23809  elfg  23814  ufilss  23848  fixufil  23865  cfinufil  23871  ufinffr  23872  ufilen  23873  fin1aufil  23875  flimclslem  23927  hauspwpwf1  23930  supnfcls  23963  flimfnfcls  23971  ptcmplem1  23995  tsmsfbas  24071  blfvalps  24326  blfps  24349  blf  24350  bcthlem5  25273  minveclem3b  25373  sigaclcuni  34268  sigaclcu2  34270  pwsiga  34280  erdsze2lem2  35392  cvmsval  35454  cvmsss2  35462  neibastop2lem  36548  tailf  36563  pibt2  37729  fin2so  37919  sdclem1  38055  elrfirn  43126  elrfirn2  43127  istopclsd  43131  nacsfix  43143  dnnumch1  43475  inpw  49258