Theorem elpw2g 5299

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 4567	. 2 ⊢ (𝐴 ∈ 𝒫 𝐵 → 𝐴 ⊆ 𝐵)
2		ssexg 5285	. . . 4 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → 𝐴 ∈ V)
3		elpwg 4563	. . . . 5 ⊢ (𝐴 ∈ V → (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵))
4	3	biimparc 485	. . . 4 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐴 ∈ V) → 𝐴 ∈ 𝒫 𝐵)
5	2, 4	syldan 603	. . 3 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → 𝐴 ∈ 𝒫 𝐵)
6	5	expcom 419	. 2 ⊢ (𝐵 ∈ 𝑉 → (𝐴 ⊆ 𝐵 → 𝐴 ∈ 𝒫 𝐵))
7	1, 6	impbid2 229	1 ⊢ (𝐵 ∈ 𝑉 → (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∈ wcel 2147  Vcvv 3454   ⊆ wss 3900  𝒫 cpw 4560

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-sep 5252

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-v 3456  df-ss 3901  df-in 4094  df-pw 4562

This theorem is used by:  elpw2  5300  rabelpw  5302  difelpw  5319  pw2f1olem  9125  fineqvlem  9282  elfir  9431  r1sscl  9816  tskwe  10055  dfac8alem  10132  acni2  10149  fin1ai  10395  fin2i  10397  fin23lem7  10418  fin23lem11  10419  isfin2-2  10421  fin23lem39  10452  isf34lem1  10474  isf34lem2  10475  isf34lem4  10479  isf34lem5  10480  fin1a2lem12  10513  canthnumlem  10757  tsken  10863  tskss  10867  gruss  10905  ismre  17786  mreintcl  17791  mremre  17800  submre  17801  mrcval  17810  mrccl  17811  mrcun  17822  ismri  17831  acsfiel  17854  isacs1i  17857  catcoppccl  18318  acsdrsel  18743  acsdrscl  18746  acsficl  18747  pmtrval  19692  pmtrrn  19698  istopg  23240  uniopn  23242  iscld  23372  ntrval  23381  clsval  23382  discld  23434  mretopd  23437  neival  23447  isnei  23448  lpval  23484  restdis  23523  ordtbaslem  23533  ordtuni  23535  cndis  23636  tgcmp  23746  hauscmplem  23751  comppfsc  23878  elkgen  23882  xkoopn  23935  elqtop  24043  kqffn  24071  isfbas  24175  filss  24199  snfbas  24212  elfg  24217  ufilss  24251  fixufil  24268  cfinufil  24274  ufinffr  24275  ufilen  24276  fin1aufil  24278  flimclslem  24330  hauspwpwf1  24333  supnfcls  24366  flimfnfcls  24374  ptcmplem1  24398  tsmsfbas  24474  blfvalps  24729  blfps  24752  blf  24753  bcthlem5  25676  minveclem3b  25776  sigaclcuni  34817  sigaclcu2  34819  pwsiga  34829  erdsze2lem2  36135  cvmsval  36197  cvmsss2  36205  neibastop2lem  37325  tailf  37340  pibt2  38531  fin2so  38721  sdclem1  38868  elrfirn  43897  elrfirn2  43898  istopclsd  43902  nacsfix  43914  dnnumch1  44242  inpw  50139