Theorem elpw2g 5290

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

Syntax hints:   → wi 4   ↔ wb 206   ∈ wcel 2109  Vcvv 3450   ⊆ wss 3916  𝒫 cpw 4565

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702  ax-sep 5253

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-rab 3409  df-v 3452  df-in 3923  df-ss 3933  df-pw 4567

This theorem is referenced by:  elpw2  5291  rabelpw  5293  difelpw  5311  pw2f1olem  9049  fineqvlem  9215  elfir  9372  r1sscl  9744  tskwe  9909  dfac8alem  9988  acni2  10005  fin1ai  10252  fin2i  10254  fin23lem7  10275  fin23lem11  10276  isfin2-2  10278  fin23lem39  10309  isf34lem1  10331  isf34lem2  10332  isf34lem4  10336  isf34lem5  10337  fin1a2lem12  10370  canthnumlem  10607  tsken  10713  tskss  10717  gruss  10755  ismre  17557  mreintcl  17562  mremre  17571  submre  17572  mrcval  17577  mrccl  17578  mrcun  17589  ismri  17598  acsfiel  17621  isacs1i  17624  catcoppccl  18085  acsdrsel  18508  acsdrscl  18511  acsficl  18512  pmtrval  19387  pmtrrn  19393  istopg  22788  uniopn  22790  iscld  22920  ntrval  22929  clsval  22930  discld  22982  mretopd  22985  neival  22995  isnei  22996  lpval  23032  restdis  23071  ordtbaslem  23081  ordtuni  23083  cndis  23184  tgcmp  23294  hauscmplem  23299  comppfsc  23425  elkgen  23429  xkoopn  23482  elqtop  23590  kqffn  23618  isfbas  23722  filss  23746  snfbas  23759  elfg  23764  ufilss  23798  fixufil  23815  cfinufil  23821  ufinffr  23822  ufilen  23823  fin1aufil  23825  flimclslem  23877  hauspwpwf1  23880  supnfcls  23913  flimfnfcls  23921  ptcmplem1  23945  tsmsfbas  24021  blfvalps  24277  blfps  24300  blf  24301  bcthlem5  25234  minveclem3b  25334  sigaclcuni  34114  sigaclcu2  34116  pwsiga  34126  erdsze2lem2  35191  cvmsval  35253  cvmsss2  35261  neibastop2lem  36343  tailf  36358  pibt2  37400  fin2so  37596  sdclem1  37732  elrfirn  42676  elrfirn2  42677  istopclsd  42681  nacsfix  42693  dnnumch1  43026  inpw  48803