Theorem elpw2g 5304

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 5294	. . . 4 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → 𝐴 ∈ V)
3		elpwg 4568	. . . . 5 ⊢ (𝐴 ∈ V → (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵))
4	3	biimparc 484	. . . 4 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐴 ∈ V) → 𝐴 ∈ 𝒫 𝐵)
5	2, 4	syldan 602	. . 3 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → 𝐴 ∈ 𝒫 𝐵)
6	5	expcom 418	. 2 ⊢ (𝐵 ∈ 𝑉 → (𝐴 ⊆ 𝐵 → 𝐴 ∈ 𝒫 𝐵))
7	1, 6	impbid2 229	1 ⊢ (𝐵 ∈ 𝑉 → (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵))

Syntax hints:   → wi 4   ↔ wb 209   ∈ wcel 2149  Vcvv 3461   ⊆ wss 3911  𝒫 cpw 4565

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741  ax-sep 5259

This theorem depends on definitions:  df-bi 210  df-an 401  df-3an 1103  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rab 3423  df-v 3463  df-in 3918  df-ss 3928  df-pw 4567

This theorem is referenced by:  elpw2  5305  rabelpw  5307  difelpw  5325  pw2f1olem  9069  fineqvlem  9226  elfir  9375  r1sscl  9757  tskwe  9936  dfac8alem  10013  acni2  10030  fin1ai  10277  fin2i  10279  fin23lem7  10300  fin23lem11  10301  isfin2-2  10303  fin23lem39  10334  isf34lem1  10356  isf34lem2  10357  isf34lem4  10361  isf34lem5  10362  fin1a2lem12  10395  canthnumlem  10633  tsken  10739  tskss  10743  gruss  10781  ismre  17642  mreintcl  17647  mremre  17656  submre  17657  mrcval  17666  mrccl  17667  mrcun  17678  ismri  17687  acsfiel  17710  isacs1i  17713  catcoppccl  18174  acsdrsel  18599  acsdrscl  18602  acsficl  18603  pmtrval  19521  pmtrrn  19527  istopg  23021  uniopn  23023  iscld  23153  ntrval  23162  clsval  23163  discld  23215  mretopd  23218  neival  23228  isnei  23229  lpval  23265  restdis  23304  ordtbaslem  23314  ordtuni  23316  cndis  23417  tgcmp  23527  hauscmplem  23532  comppfsc  23658  elkgen  23662  xkoopn  23715  elqtop  23823  kqffn  23851  isfbas  23955  filss  23979  snfbas  23992  elfg  23997  ufilss  24031  fixufil  24048  cfinufil  24054  ufinffr  24055  ufilen  24056  fin1aufil  24058  flimclslem  24110  hauspwpwf1  24113  supnfcls  24146  flimfnfcls  24154  ptcmplem1  24178  tsmsfbas  24254  blfvalps  24509  blfps  24532  blf  24533  bcthlem5  25456  minveclem3b  25556  sigaclcuni  34453  sigaclcu2  34455  pwsiga  34465  erdsze2lem2  35629  cvmsval  35691  cvmsss2  35699  neibastop2lem  36794  tailf  36809  pibt2  37986  fin2so  38181  sdclem1  38317  elrfirn  43353  elrfirn2  43354  istopclsd  43358  nacsfix  43370  dnnumch1  43698  inpw  49523