Theorem elpw2g 5291

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 4564	. 2 ⊢ (𝐴 ∈ 𝒫 𝐵 → 𝐴 ⊆ 𝐵)
2		ssexg 5281	. . . 4 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → 𝐴 ∈ V)
3		elpwg 4560	. . . . 5 ⊢ (𝐴 ∈ V → (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵))
4	3	biimparc 483	. . . 4 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐴 ∈ V) → 𝐴 ∈ 𝒫 𝐵)
5	2, 4	syldan 600	. . 3 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → 𝐴 ∈ 𝒫 𝐵)
6	5	expcom 417	. 2 ⊢ (𝐵 ∈ 𝑉 → (𝐴 ⊆ 𝐵 → 𝐴 ∈ 𝒫 𝐵))
7	1, 6	impbid2 228	1 ⊢ (𝐵 ∈ 𝑉 → (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵))

Syntax hints:   → wi 4   ↔ wb 208   ∈ wcel 2144  Vcvv 3456   ⊆ wss 3906  𝒫 cpw 4557

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-ext 2736  ax-sep 5248

This theorem depends on definitions:  df-bi 209  df-an 400  df-3an 1101  df-tru 1565  df-ex 1802  df-sb 2093  df-clab 2743  df-cleq 2756  df-clel 2839  df-rab 3417  df-v 3458  df-in 3913  df-ss 3923  df-pw 4559

This theorem is referenced by:  elpw2  5292  rabelpw  5294  difelpw  5312  pw2f1olem  9055  fineqvlem  9212  elfir  9363  r1sscl  9745  tskwe  9910  dfac8alem  9987  acni2  10004  fin1ai  10252  fin2i  10254  fin23lem7  10275  fin23lem11  10276  isfin2-2  10278  fin23lem39  10309  isf34lem1  10331  isf34lem2  10332  isf34lem4  10336  isf34lem5  10337  fin1a2lem12  10370  canthnumlem  10608  tsken  10714  tskss  10718  gruss  10756  ismre  17620  mreintcl  17625  mremre  17634  submre  17635  mrcval  17644  mrccl  17645  mrcun  17656  ismri  17665  acsfiel  17688  isacs1i  17691  catcoppccl  18152  acsdrsel  18577  acsdrscl  18580  acsficl  18581  pmtrval  19493  pmtrrn  19499  istopg  22957  uniopn  22959  iscld  23089  ntrval  23098  clsval  23099  discld  23151  mretopd  23154  neival  23164  isnei  23165  lpval  23201  restdis  23240  ordtbaslem  23250  ordtuni  23252  cndis  23353  tgcmp  23463  hauscmplem  23468  comppfsc  23594  elkgen  23598  xkoopn  23651  elqtop  23759  kqffn  23787  isfbas  23891  filss  23915  snfbas  23928  elfg  23933  ufilss  23967  fixufil  23984  cfinufil  23990  ufinffr  23991  ufilen  23992  fin1aufil  23994  flimclslem  24046  hauspwpwf1  24049  supnfcls  24082  flimfnfcls  24090  ptcmplem1  24114  tsmsfbas  24190  blfvalps  24445  blfps  24468  blf  24469  bcthlem5  25392  minveclem3b  25492  sigaclcuni  34417  sigaclcu2  34419  pwsiga  34429  erdsze2lem2  35559  cvmsval  35621  cvmsss2  35629  neibastop2lem  36725  tailf  36740  pibt2  37916  fin2so  38111  sdclem1  38247  elrfirn  43281  elrfirn2  43282  istopclsd  43286  nacsfix  43298  dnnumch1  43626  inpw  49451