Theorem elpw2g 5351

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 4629	. 2 ⊢ (𝐴 ∈ 𝒫 𝐵 → 𝐴 ⊆ 𝐵)
2		ssexg 5341	. . . 4 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → 𝐴 ∈ V)
3		elpwg 4625	. . . . 5 ⊢ (𝐴 ∈ V → (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵))
4	3	biimparc 479	. . . 4 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐴 ∈ V) → 𝐴 ∈ 𝒫 𝐵)
5	2, 4	syldan 590	. . 3 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → 𝐴 ∈ 𝒫 𝐵)
6	5	expcom 413	. 2 ⊢ (𝐵 ∈ 𝑉 → (𝐴 ⊆ 𝐵 → 𝐴 ∈ 𝒫 𝐵))
7	1, 6	impbid2 226	1 ⊢ (𝐵 ∈ 𝑉 → (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵))

Syntax hints:   → wi 4   ↔ wb 206   ∈ wcel 2108  Vcvv 3488   ⊆ wss 3976  𝒫 cpw 4622

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-sep 5317

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1089  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-v 3490  df-in 3983  df-ss 3993  df-pw 4624

This theorem is referenced by:  elpw2  5352  rabelpw  5354  difelpw  5372  pw2f1olem  9142  fineqvlem  9325  elfir  9484  r1sscl  9854  tskwe  10019  dfac8alem  10098  acni2  10115  fin1ai  10362  fin2i  10364  fin23lem7  10385  fin23lem11  10386  isfin2-2  10388  fin23lem39  10419  isf34lem1  10441  isf34lem2  10442  isf34lem4  10446  isf34lem5  10447  fin1a2lem12  10480  canthnumlem  10717  tsken  10823  tskss  10827  gruss  10865  ismre  17648  mreintcl  17653  mremre  17662  submre  17663  mrcval  17668  mrccl  17669  mrcun  17680  ismri  17689  acsfiel  17712  isacs1i  17715  catcoppccl  18184  catcoppcclOLD  18185  acsdrsel  18613  acsdrscl  18616  acsficl  18617  pmtrval  19493  pmtrrn  19499  istopg  22922  uniopn  22924  iscld  23056  ntrval  23065  clsval  23066  discld  23118  mretopd  23121  neival  23131  isnei  23132  lpval  23168  restdis  23207  ordtbaslem  23217  ordtuni  23219  cndis  23320  tgcmp  23430  hauscmplem  23435  comppfsc  23561  elkgen  23565  xkoopn  23618  elqtop  23726  kqffn  23754  isfbas  23858  filss  23882  snfbas  23895  elfg  23900  ufilss  23934  fixufil  23951  cfinufil  23957  ufinffr  23958  ufilen  23959  fin1aufil  23961  flimclslem  24013  hauspwpwf1  24016  supnfcls  24049  flimfnfcls  24057  ptcmplem1  24081  tsmsfbas  24157  blfvalps  24414  blfps  24437  blf  24438  bcthlem5  25381  minveclem3b  25481  sigaclcuni  34082  sigaclcu2  34084  pwsiga  34094  erdsze2lem2  35172  cvmsval  35234  cvmsss2  35242  neibastop2lem  36326  tailf  36341  pibt2  37383  fin2so  37567  sdclem1  37703  elrfirn  42651  elrfirn2  42652  istopclsd  42656  nacsfix  42668  dnnumch1  43001  inpw  48550