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 4542	. 2 ⊢ (𝐴 ∈ 𝒫 𝐵 → 𝐴 ⊆ 𝐵)
2		ssexg 5247	. . . 4 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → 𝐴 ∈ V)
3		elpwg 4536	. . . . 5 ⊢ (𝐴 ∈ V → (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵))
4	3	biimparc 480	. . . 4 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐴 ∈ V) → 𝐴 ∈ 𝒫 𝐵)
5	2, 4	syldan 591	. . 3 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → 𝐴 ∈ 𝒫 𝐵)
6	5	expcom 414	. 2 ⊢ (𝐵 ∈ 𝑉 → (𝐴 ⊆ 𝐵 → 𝐴 ∈ 𝒫 𝐵))
7	1, 6	impbid2 225	1 ⊢ (𝐵 ∈ 𝑉 → (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵))

Syntax hints:   → wi 4   ↔ wb 205   ∈ wcel 2106  Vcvv 3432   ⊆ wss 3887  𝒫 cpw 4533

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709  ax-sep 5223

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-rab 3073  df-v 3434  df-in 3894  df-ss 3904  df-pw 4535

This theorem is referenced by:  elpw2  5269  elpwi2OLD  5271  pwnss  5272  difelpw  5274  rabelpw  5275  pw2f1olem  8863  fineqvlem  9037  elfir  9174  r1sscl  9543  tskwe  9708  dfac8alem  9785  acni2  9802  fin1ai  10049  fin2i  10051  fin23lem7  10072  fin23lem11  10073  isfin2-2  10075  fin23lem39  10106  isf34lem1  10128  isf34lem2  10129  isf34lem4  10133  isf34lem5  10134  fin1a2lem12  10167  canthnumlem  10404  tsken  10510  tskss  10514  gruss  10552  ismre  17299  mreintcl  17304  mremre  17313  submre  17314  mrcval  17319  mrccl  17320  mrcun  17331  ismri  17340  acsfiel  17363  isacs1i  17366  catcoppccl  17832  catcoppcclOLD  17833  acsdrsel  18261  acsdrscl  18264  acsficl  18265  pmtrval  19059  pmtrrn  19065  istopg  22044  uniopn  22046  iscld  22178  ntrval  22187  clsval  22188  discld  22240  mretopd  22243  neival  22253  isnei  22254  lpval  22290  restdis  22329  ordtbaslem  22339  ordtuni  22341  cndis  22442  tgcmp  22552  hauscmplem  22557  comppfsc  22683  elkgen  22687  xkoopn  22740  elqtop  22848  kqffn  22876  isfbas  22980  filss  23004  snfbas  23017  elfg  23022  ufilss  23056  fixufil  23073  cfinufil  23079  ufinffr  23080  ufilen  23081  fin1aufil  23083  flimclslem  23135  hauspwpwf1  23138  supnfcls  23171  flimfnfcls  23179  ptcmplem1  23203  tsmsfbas  23279  blfvalps  23536  blfps  23559  blf  23560  bcthlem5  24492  minveclem3b  24592  sigaclcuni  32086  sigaclcu2  32088  pwsiga  32098  erdsze2lem2  33166  cvmsval  33228  cvmsss2  33236  neibastop2lem  34549  tailf  34564  pibt2  35588  fin2so  35764  sdclem1  35901  elrfirn  40517  elrfirn2  40518  istopclsd  40522  nacsfix  40534  dnnumch1  40869  inpw  46164