Theorem elpw2g 5279

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 4562	. 2 ⊢ (𝐴 ∈ 𝒫 𝐵 → 𝐴 ⊆ 𝐵)
2		ssexg 5269	. . . 4 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → 𝐴 ∈ V)
3		elpwg 4558	. . . . 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 3441   ⊆ wss 3902  𝒫 cpw 4555

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 5242

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 3401  df-v 3443  df-in 3909  df-ss 3919  df-pw 4557

This theorem is referenced by:  elpw2  5280  rabelpw  5282  difelpw  5300  pw2f1olem  9013  fineqvlem  9170  elfir  9322  r1sscl  9701  tskwe  9866  dfac8alem  9943  acni2  9960  fin1ai  10207  fin2i  10209  fin23lem7  10230  fin23lem11  10231  isfin2-2  10233  fin23lem39  10264  isf34lem1  10286  isf34lem2  10287  isf34lem4  10291  isf34lem5  10292  fin1a2lem12  10325  canthnumlem  10563  tsken  10669  tskss  10673  gruss  10711  ismre  17513  mreintcl  17518  mremre  17527  submre  17528  mrcval  17537  mrccl  17538  mrcun  17549  ismri  17558  acsfiel  17581  isacs1i  17584  catcoppccl  18045  acsdrsel  18470  acsdrscl  18473  acsficl  18474  pmtrval  19384  pmtrrn  19390  istopg  22843  uniopn  22845  iscld  22975  ntrval  22984  clsval  22985  discld  23037  mretopd  23040  neival  23050  isnei  23051  lpval  23087  restdis  23126  ordtbaslem  23136  ordtuni  23138  cndis  23239  tgcmp  23349  hauscmplem  23354  comppfsc  23480  elkgen  23484  xkoopn  23537  elqtop  23645  kqffn  23673  isfbas  23777  filss  23801  snfbas  23814  elfg  23819  ufilss  23853  fixufil  23870  cfinufil  23876  ufinffr  23877  ufilen  23878  fin1aufil  23880  flimclslem  23932  hauspwpwf1  23935  supnfcls  23968  flimfnfcls  23976  ptcmplem1  24000  tsmsfbas  24076  blfvalps  24331  blfps  24354  blf  24355  bcthlem5  25288  minveclem3b  25388  sigaclcuni  34256  sigaclcu2  34258  pwsiga  34268  erdsze2lem2  35379  cvmsval  35441  cvmsss2  35449  neibastop2lem  36535  tailf  36550  pibt2  37593  fin2so  37779  sdclem1  37915  elrfirn  42973  elrfirn2  42974  istopclsd  42978  nacsfix  42990  dnnumch1  43322  inpw  49106