Theorem elpw2g 5342

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 4607	. 2 ⊢ (𝐴 ∈ 𝒫 𝐵 → 𝐴 ⊆ 𝐵)
2		ssexg 5321	. . . 4 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → 𝐴 ∈ V)
3		elpwg 4603	. . . . 5 ⊢ (𝐴 ∈ V → (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵))
4	3	biimparc 481	. . . 4 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐴 ∈ V) → 𝐴 ∈ 𝒫 𝐵)
5	2, 4	syldan 592	. . 3 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → 𝐴 ∈ 𝒫 𝐵)
6	5	expcom 415	. 2 ⊢ (𝐵 ∈ 𝑉 → (𝐴 ⊆ 𝐵 → 𝐴 ∈ 𝒫 𝐵))
7	1, 6	impbid2 225	1 ⊢ (𝐵 ∈ 𝑉 → (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵))

Syntax hints:   → wi 4   ↔ wb 205   ∈ wcel 2107  Vcvv 3475   ⊆ wss 3946  𝒫 cpw 4600

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-sep 5297

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477  df-in 3953  df-ss 3963  df-pw 4602

This theorem is referenced by:  elpw2  5343  elpwi2OLD  5345  pwnss  5347  difelpw  5349  rabelpw  5350  pw2f1olem  9071  fineqvlem  9257  elfir  9405  r1sscl  9775  tskwe  9940  dfac8alem  10019  acni2  10036  fin1ai  10283  fin2i  10285  fin23lem7  10306  fin23lem11  10307  isfin2-2  10309  fin23lem39  10340  isf34lem1  10362  isf34lem2  10363  isf34lem4  10367  isf34lem5  10368  fin1a2lem12  10401  canthnumlem  10638  tsken  10744  tskss  10748  gruss  10786  ismre  17529  mreintcl  17534  mremre  17543  submre  17544  mrcval  17549  mrccl  17550  mrcun  17561  ismri  17570  acsfiel  17593  isacs1i  17596  catcoppccl  18062  catcoppcclOLD  18063  acsdrsel  18491  acsdrscl  18494  acsficl  18495  pmtrval  19311  pmtrrn  19317  istopg  22378  uniopn  22380  iscld  22512  ntrval  22521  clsval  22522  discld  22574  mretopd  22577  neival  22587  isnei  22588  lpval  22624  restdis  22663  ordtbaslem  22673  ordtuni  22675  cndis  22776  tgcmp  22886  hauscmplem  22891  comppfsc  23017  elkgen  23021  xkoopn  23074  elqtop  23182  kqffn  23210  isfbas  23314  filss  23338  snfbas  23351  elfg  23356  ufilss  23390  fixufil  23407  cfinufil  23413  ufinffr  23414  ufilen  23415  fin1aufil  23417  flimclslem  23469  hauspwpwf1  23472  supnfcls  23505  flimfnfcls  23513  ptcmplem1  23537  tsmsfbas  23613  blfvalps  23870  blfps  23893  blf  23894  bcthlem5  24826  minveclem3b  24926  sigaclcuni  33053  sigaclcu2  33055  pwsiga  33065  erdsze2lem2  34132  cvmsval  34194  cvmsss2  34202  neibastop2lem  35182  tailf  35197  pibt2  36235  fin2so  36412  sdclem1  36548  elrfirn  41365  elrfirn2  41366  istopclsd  41370  nacsfix  41382  dnnumch1  41718  inpw  47404