Theorem elpw2g 5273

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 4556	. 2 ⊢ (𝐴 ∈ 𝒫 𝐵 → 𝐴 ⊆ 𝐵)
2		ssexg 5263	. . . 4 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → 𝐴 ∈ V)
3		elpwg 4552	. . . . 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 2111  Vcvv 3436   ⊆ wss 3897  𝒫 cpw 4549

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703  ax-sep 5236

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-v 3438  df-in 3904  df-ss 3914  df-pw 4551

This theorem is referenced by:  elpw2  5274  rabelpw  5276  difelpw  5294  pw2f1olem  9000  fineqvlem  9156  elfir  9305  r1sscl  9684  tskwe  9849  dfac8alem  9926  acni2  9943  fin1ai  10190  fin2i  10192  fin23lem7  10213  fin23lem11  10214  isfin2-2  10216  fin23lem39  10247  isf34lem1  10269  isf34lem2  10270  isf34lem4  10274  isf34lem5  10275  fin1a2lem12  10308  canthnumlem  10545  tsken  10651  tskss  10655  gruss  10693  ismre  17498  mreintcl  17503  mremre  17512  submre  17513  mrcval  17522  mrccl  17523  mrcun  17534  ismri  17543  acsfiel  17566  isacs1i  17569  catcoppccl  18030  acsdrsel  18455  acsdrscl  18458  acsficl  18459  pmtrval  19369  pmtrrn  19375  istopg  22816  uniopn  22818  iscld  22948  ntrval  22957  clsval  22958  discld  23010  mretopd  23013  neival  23023  isnei  23024  lpval  23060  restdis  23099  ordtbaslem  23109  ordtuni  23111  cndis  23212  tgcmp  23322  hauscmplem  23327  comppfsc  23453  elkgen  23457  xkoopn  23510  elqtop  23618  kqffn  23646  isfbas  23750  filss  23774  snfbas  23787  elfg  23792  ufilss  23826  fixufil  23843  cfinufil  23849  ufinffr  23850  ufilen  23851  fin1aufil  23853  flimclslem  23905  hauspwpwf1  23908  supnfcls  23941  flimfnfcls  23949  ptcmplem1  23973  tsmsfbas  24049  blfvalps  24304  blfps  24327  blf  24328  bcthlem5  25261  minveclem3b  25361  sigaclcuni  34138  sigaclcu2  34140  pwsiga  34150  erdsze2lem2  35255  cvmsval  35317  cvmsss2  35325  neibastop2lem  36411  tailf  36426  pibt2  37468  fin2so  37653  sdclem1  37789  elrfirn  42793  elrfirn2  42794  istopclsd  42798  nacsfix  42810  dnnumch1  43142  inpw  48930