Theorem elpw2g 4754

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 4117	. 2 ⊢ (𝐴 ∈ 𝒫 𝐵 → 𝐴 ⊆ 𝐵)
2		ssexg 4732	. . . 4 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → 𝐴 ∈ V)
3		elpwg 4116	. . . . 5 ⊢ (𝐴 ∈ V → (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵))
4	3	biimparc 503	. . . 4 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐴 ∈ V) → 𝐴 ∈ 𝒫 𝐵)
5	2, 4	syldan 486	. . 3 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → 𝐴 ∈ 𝒫 𝐵)
6	5	expcom 450	. 2 ⊢ (𝐵 ∈ 𝑉 → (𝐴 ⊆ 𝐵 → 𝐴 ∈ 𝒫 𝐵))
7	1, 6	impbid2 215	1 ⊢ (𝐵 ∈ 𝑉 → (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵))

Syntax hints:   → wi 4   ↔ wb 195   ∈ wcel 1977  Vcvv 3173   ⊆ wss 3540  𝒫 cpw 4108

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-in 3547  df-ss 3554  df-pw 4110

This theorem is referenced by:  elpw2  4755  pwnss  4756  knatar  6507  pw2f1olem  7949  fineqvlem  8059  elfir  8204  marypha1  8223  r1sscl  8531  tskwe  8659  dfac8alem  8735  acni2  8752  fin1ai  8998  fin2i  9000  fin23lem7  9021  fin23lem11  9022  isfin2-2  9024  fin23lem39  9055  isf34lem1  9077  isf34lem2  9078  isf34lem4  9082  isf34lem5  9083  fin1a2lem12  9116  canthnumlem  9349  canthp1lem2  9354  wunss  9413  tsken  9455  tskss  9459  gruss  9497  ramub1lem1  15568  ismre  16073  mreintcl  16078  mremre  16087  submre  16088  mrcval  16093  mrccl  16094  mrcun  16105  ismri  16114  mreexd  16125  mreexexlem4d  16130  acsfiel  16138  isacs1i  16141  catcoppccl  16581  acsdrsel  16990  acsdrscl  16993  acsficl  16994  pmtrval  17694  pmtrrn  17700  opsrval  19295  istopg  20525  uniopn  20527  iscld  20641  ntrval  20650  clsval  20651  discld  20703  mretopd  20706  neival  20716  isnei  20717  lpval  20753  restdis  20792  ordtbaslem  20802  ordtuni  20804  cncls  20888  cndis  20905  tgcmp  21014  hauscmplem  21019  comppfsc  21145  elkgen  21149  xkoopn  21202  elqtop  21310  kqffn  21338  isfbas  21443  filss  21467  snfbas  21480  elfg  21485  fbasrn  21498  ufilss  21519  fixufil  21536  cfinufil  21542  ufinffr  21543  ufilen  21544  fin1aufil  21546  rnelfmlem  21566  flimclslem  21598  hauspwpwf1  21601  supnfcls  21634  flimfnfcls  21642  ptcmplem1  21666  tsmsfbas  21741  blfvalps  21998  blfps  22021  blf  22022  bcthlem5  22933  minveclem3b  23007  sigaclcuni  29508  sigaclcu2  29510  pwsiga  29520  erdsze2lem2  30440  cvmsval  30502  cvmsss2  30510  neibastop2lem  31525  tailf  31540  fin2so  32566  sdclem1  32709  elrfirn  36276  elrfirn2  36277  istopclsd  36281  nacsfix  36293  dnnumch1  36632  elpwi2  38291