Theorem elpw2g 5303

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 4568	. 2 ⊢ (𝐴 ∈ 𝒫 𝐵 → 𝐴 ⊆ 𝐵)
2		ssexg 5289	. . . 4 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → 𝐴 ∈ V)
3		elpwg 4564	. . . . 5 ⊢ (𝐴 ∈ V → (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵))
4	3	biimparc 484	. . . 4 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐴 ∈ V) → 𝐴 ∈ 𝒫 𝐵)
5	2, 4	syldan 602	. . 3 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → 𝐴 ∈ 𝒫 𝐵)
6	5	expcom 418	. 2 ⊢ (𝐵 ∈ 𝑉 → (𝐴 ⊆ 𝐵 → 𝐴 ∈ 𝒫 𝐵))
7	1, 6	impbid2 229	1 ⊢ (𝐵 ∈ 𝑉 → (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∈ wcel 2142  Vcvv 3454   ⊆ wss 3904  𝒫 cpw 4561

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-ext 2734  ax-sep 5256

This proof depends on definitions:  df-bi 210  df-an 401  df-3an 1104  df-tru 1572  df-ex 1809  df-sb 2096  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3416  df-v 3456  df-in 3911  df-ss 3921  df-pw 4563

This theorem is used by:  elpw2  5304  rabelpw  5306  difelpw  5323  pw2f1olem  9067  fineqvlem  9224  elfir  9373  r1sscl  9755  tskwe  9943  dfac8alem  10020  acni2  10037  fin1ai  10283  fin2i  10285  fin23lem7  10306  fin23lem11  10307  isfin2-2  10309  fin23lem39  10340  isf34lem1  10362  isf34lem2  10363  isf34lem4  10367  isf34lem5  10368  fin1a2lem12  10401  canthnumlem  10639  tsken  10745  tskss  10749  gruss  10787  ismre  17648  mreintcl  17653  mremre  17662  submre  17663  mrcval  17672  mrccl  17673  mrcun  17684  ismri  17693  acsfiel  17716  isacs1i  17719  catcoppccl  18180  acsdrsel  18605  acsdrscl  18608  acsficl  18609  pmtrval  19527  pmtrrn  19533  istopg  23063  uniopn  23065  iscld  23195  ntrval  23204  clsval  23205  discld  23257  mretopd  23260  neival  23270  isnei  23271  lpval  23307  restdis  23346  ordtbaslem  23356  ordtuni  23358  cndis  23459  tgcmp  23569  hauscmplem  23574  comppfsc  23700  elkgen  23704  xkoopn  23757  elqtop  23865  kqffn  23893  isfbas  23997  filss  24021  snfbas  24034  elfg  24039  ufilss  24073  fixufil  24090  cfinufil  24096  ufinffr  24097  ufilen  24098  fin1aufil  24100  flimclslem  24152  hauspwpwf1  24155  supnfcls  24188  flimfnfcls  24196  ptcmplem1  24220  tsmsfbas  24296  blfvalps  24551  blfps  24574  blf  24575  bcthlem5  25498  minveclem3b  25598  sigaclcuni  34517  sigaclcu2  34519  pwsiga  34529  erdsze2lem2  35704  cvmsval  35766  cvmsss2  35774  neibastop2lem  36899  tailf  36914  pibt2  38091  fin2so  38286  sdclem1  38422  elrfirn  43454  elrfirn2  43455  istopclsd  43459  nacsfix  43471  dnnumch1  43799  inpw  49631