Theorem elpw2g 5346

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 4610	. 2 ⊢ (𝐴 ∈ 𝒫 𝐵 → 𝐴 ⊆ 𝐵)
2		ssexg 5323	. . . 4 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → 𝐴 ∈ V)
3		elpwg 4606	. . . . 5 ⊢ (𝐴 ∈ V → (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵))
4	3	biimparc 478	. . . 4 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐴 ∈ V) → 𝐴 ∈ 𝒫 𝐵)
5	2, 4	syldan 589	. . 3 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → 𝐴 ∈ 𝒫 𝐵)
6	5	expcom 412	. 2 ⊢ (𝐵 ∈ 𝑉 → (𝐴 ⊆ 𝐵 → 𝐴 ∈ 𝒫 𝐵))
7	1, 6	impbid2 225	1 ⊢ (𝐵 ∈ 𝑉 → (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵))

Syntax hints:   → wi 4   ↔ wb 205   ∈ wcel 2098  Vcvv 3463   ⊆ wss 3945  𝒫 cpw 4603

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696  ax-sep 5299

This theorem depends on definitions:  df-bi 206  df-an 395  df-3an 1086  df-tru 1536  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-rab 3420  df-v 3465  df-in 3952  df-ss 3962  df-pw 4605

This theorem is referenced by:  elpw2  5347  pwnss  5350  difelpw  5352  rabelpw  5353  pw2f1olem  9099  fineqvlem  9285  elfir  9438  r1sscl  9808  tskwe  9973  dfac8alem  10052  acni2  10069  fin1ai  10316  fin2i  10318  fin23lem7  10339  fin23lem11  10340  isfin2-2  10342  fin23lem39  10373  isf34lem1  10395  isf34lem2  10396  isf34lem4  10400  isf34lem5  10401  fin1a2lem12  10434  canthnumlem  10671  tsken  10777  tskss  10781  gruss  10819  ismre  17570  mreintcl  17575  mremre  17584  submre  17585  mrcval  17590  mrccl  17591  mrcun  17602  ismri  17611  acsfiel  17634  isacs1i  17637  catcoppccl  18106  catcoppcclOLD  18107  acsdrsel  18535  acsdrscl  18538  acsficl  18539  pmtrval  19411  pmtrrn  19417  istopg  22828  uniopn  22830  iscld  22962  ntrval  22971  clsval  22972  discld  23024  mretopd  23027  neival  23037  isnei  23038  lpval  23074  restdis  23113  ordtbaslem  23123  ordtuni  23125  cndis  23226  tgcmp  23336  hauscmplem  23341  comppfsc  23467  elkgen  23471  xkoopn  23524  elqtop  23632  kqffn  23660  isfbas  23764  filss  23788  snfbas  23801  elfg  23806  ufilss  23840  fixufil  23857  cfinufil  23863  ufinffr  23864  ufilen  23865  fin1aufil  23867  flimclslem  23919  hauspwpwf1  23922  supnfcls  23955  flimfnfcls  23963  ptcmplem1  23987  tsmsfbas  24063  blfvalps  24320  blfps  24343  blf  24344  bcthlem5  25287  minveclem3b  25387  sigaclcuni  33824  sigaclcu2  33826  pwsiga  33836  erdsze2lem2  34901  cvmsval  34963  cvmsss2  34971  neibastop2lem  35931  tailf  35946  pibt2  36983  fin2so  37167  sdclem1  37303  elrfirn  42197  elrfirn2  42198  istopclsd  42202  nacsfix  42214  dnnumch1  42550  inpw  48017