Theorem elpw2g 5340

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 4605	. 2 ⊢ (𝐴 ∈ 𝒫 𝐵 → 𝐴 ⊆ 𝐵)
2		ssexg 5317	. . . 4 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → 𝐴 ∈ V)
3		elpwg 4601	. . . . 5 ⊢ (𝐴 ∈ V → (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵))
4	3	biimparc 479	. . . 4 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐴 ∈ V) → 𝐴 ∈ 𝒫 𝐵)
5	2, 4	syldan 590	. . 3 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → 𝐴 ∈ 𝒫 𝐵)
6	5	expcom 413	. 2 ⊢ (𝐵 ∈ 𝑉 → (𝐴 ⊆ 𝐵 → 𝐴 ∈ 𝒫 𝐵))
7	1, 6	impbid2 225	1 ⊢ (𝐵 ∈ 𝑉 → (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵))

Syntax hints:   → wi 4   ↔ wb 205   ∈ wcel 2099  Vcvv 3469   ⊆ wss 3944  𝒫 cpw 4598

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2698  ax-sep 5293

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2705  df-cleq 2719  df-clel 2805  df-rab 3428  df-v 3471  df-in 3951  df-ss 3961  df-pw 4600

This theorem is referenced by:  elpw2  5341  elpwi2OLD  5343  pwnss  5345  difelpw  5347  rabelpw  5348  pw2f1olem  9092  fineqvlem  9278  elfir  9430  r1sscl  9800  tskwe  9965  dfac8alem  10044  acni2  10061  fin1ai  10308  fin2i  10310  fin23lem7  10331  fin23lem11  10332  isfin2-2  10334  fin23lem39  10365  isf34lem1  10387  isf34lem2  10388  isf34lem4  10392  isf34lem5  10393  fin1a2lem12  10426  canthnumlem  10663  tsken  10769  tskss  10773  gruss  10811  ismre  17561  mreintcl  17566  mremre  17575  submre  17576  mrcval  17581  mrccl  17582  mrcun  17593  ismri  17602  acsfiel  17625  isacs1i  17628  catcoppccl  18097  catcoppcclOLD  18098  acsdrsel  18526  acsdrscl  18529  acsficl  18530  pmtrval  19397  pmtrrn  19403  istopg  22784  uniopn  22786  iscld  22918  ntrval  22927  clsval  22928  discld  22980  mretopd  22983  neival  22993  isnei  22994  lpval  23030  restdis  23069  ordtbaslem  23079  ordtuni  23081  cndis  23182  tgcmp  23292  hauscmplem  23297  comppfsc  23423  elkgen  23427  xkoopn  23480  elqtop  23588  kqffn  23616  isfbas  23720  filss  23744  snfbas  23757  elfg  23762  ufilss  23796  fixufil  23813  cfinufil  23819  ufinffr  23820  ufilen  23821  fin1aufil  23823  flimclslem  23875  hauspwpwf1  23878  supnfcls  23911  flimfnfcls  23919  ptcmplem1  23943  tsmsfbas  24019  blfvalps  24276  blfps  24299  blf  24300  bcthlem5  25243  minveclem3b  25343  sigaclcuni  33673  sigaclcu2  33675  pwsiga  33685  erdsze2lem2  34750  cvmsval  34812  cvmsss2  34820  neibastop2lem  35780  tailf  35795  pibt2  36832  fin2so  37015  sdclem1  37151  elrfirn  42037  elrfirn2  42038  istopclsd  42042  nacsfix  42054  dnnumch1  42390  inpw  47812