Theorem elpw2g 5288

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 4570	. 2 ⊢ (𝐴 ∈ 𝒫 𝐵 → 𝐴 ⊆ 𝐵)
2		ssexg 5278	. . . 4 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → 𝐴 ∈ V)
3		elpwg 4566	. . . . 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 3447   ⊆ wss 3914  𝒫 cpw 4563

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 2701  ax-sep 5251

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 2708  df-cleq 2721  df-clel 2803  df-rab 3406  df-v 3449  df-in 3921  df-ss 3931  df-pw 4565

This theorem is referenced by:  elpw2  5289  rabelpw  5291  difelpw  5309  pw2f1olem  9045  fineqvlem  9209  elfir  9366  r1sscl  9738  tskwe  9903  dfac8alem  9982  acni2  9999  fin1ai  10246  fin2i  10248  fin23lem7  10269  fin23lem11  10270  isfin2-2  10272  fin23lem39  10303  isf34lem1  10325  isf34lem2  10326  isf34lem4  10330  isf34lem5  10331  fin1a2lem12  10364  canthnumlem  10601  tsken  10707  tskss  10711  gruss  10749  ismre  17551  mreintcl  17556  mremre  17565  submre  17566  mrcval  17571  mrccl  17572  mrcun  17583  ismri  17592  acsfiel  17615  isacs1i  17618  catcoppccl  18079  acsdrsel  18502  acsdrscl  18505  acsficl  18506  pmtrval  19381  pmtrrn  19387  istopg  22782  uniopn  22784  iscld  22914  ntrval  22923  clsval  22924  discld  22976  mretopd  22979  neival  22989  isnei  22990  lpval  23026  restdis  23065  ordtbaslem  23075  ordtuni  23077  cndis  23178  tgcmp  23288  hauscmplem  23293  comppfsc  23419  elkgen  23423  xkoopn  23476  elqtop  23584  kqffn  23612  isfbas  23716  filss  23740  snfbas  23753  elfg  23758  ufilss  23792  fixufil  23809  cfinufil  23815  ufinffr  23816  ufilen  23817  fin1aufil  23819  flimclslem  23871  hauspwpwf1  23874  supnfcls  23907  flimfnfcls  23915  ptcmplem1  23939  tsmsfbas  24015  blfvalps  24271  blfps  24294  blf  24295  bcthlem5  25228  minveclem3b  25328  sigaclcuni  34108  sigaclcu2  34110  pwsiga  34120  erdsze2lem2  35191  cvmsval  35253  cvmsss2  35261  neibastop2lem  36348  tailf  36363  pibt2  37405  fin2so  37601  sdclem1  37737  elrfirn  42683  elrfirn2  42684  istopclsd  42688  nacsfix  42700  dnnumch1  43033  inpw  48813