Theorem elpw2g 5294

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 4563	. 2 ⊢ (𝐴 ∈ 𝒫 𝐵 → 𝐴 ⊆ 𝐵)
2		ssexg 5280	. . . 4 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → 𝐴 ∈ V)
3		elpwg 4559	. . . . 5 ⊢ (𝐴 ∈ V → (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵))
4	3	biimparc 485	. . . 4 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐴 ∈ V) → 𝐴 ∈ 𝒫 𝐵)
5	2, 4	syldan 603	. . 3 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → 𝐴 ∈ 𝒫 𝐵)
6	5	expcom 419	. 2 ⊢ (𝐵 ∈ 𝑉 → (𝐴 ⊆ 𝐵 → 𝐴 ∈ 𝒫 𝐵))
7	1, 6	impbid2 229	1 ⊢ (𝐵 ∈ 𝑉 → (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∈ wcel 2145  Vcvv 3450   ⊆ wss 3898  𝒫 cpw 4556

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732  ax-sep 5248

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-in 3905  df-ss 3915  df-pw 4558

This theorem is used by:  elpw2  5295  rabelpw  5297  difelpw  5314  pw2f1olem  9078  fineqvlem  9235  elfir  9385  r1sscl  9767  tskwe  10002  dfac8alem  10079  acni2  10096  fin1ai  10342  fin2i  10344  fin23lem7  10365  fin23lem11  10366  isfin2-2  10368  fin23lem39  10399  isf34lem1  10421  isf34lem2  10422  isf34lem4  10426  isf34lem5  10427  fin1a2lem12  10460  canthnumlem  10704  tsken  10810  tskss  10814  gruss  10852  ismre  17721  mreintcl  17726  mremre  17735  submre  17736  mrcval  17745  mrccl  17746  mrcun  17757  ismri  17766  acsfiel  17789  isacs1i  17792  catcoppccl  18253  acsdrsel  18678  acsdrscl  18681  acsficl  18682  pmtrval  19626  pmtrrn  19632  istopg  23174  uniopn  23176  iscld  23306  ntrval  23315  clsval  23316  discld  23368  mretopd  23371  neival  23381  isnei  23382  lpval  23418  restdis  23457  ordtbaslem  23467  ordtuni  23469  cndis  23570  tgcmp  23680  hauscmplem  23685  comppfsc  23812  elkgen  23816  xkoopn  23869  elqtop  23977  kqffn  24005  isfbas  24109  filss  24133  snfbas  24146  elfg  24151  ufilss  24185  fixufil  24202  cfinufil  24208  ufinffr  24209  ufilen  24210  fin1aufil  24212  flimclslem  24264  hauspwpwf1  24267  supnfcls  24300  flimfnfcls  24308  ptcmplem1  24332  tsmsfbas  24408  blfvalps  24663  blfps  24686  blf  24687  bcthlem5  25610  minveclem3b  25710  sigaclcuni  34683  sigaclcu2  34685  pwsiga  34695  erdsze2lem2  35890  cvmsval  35952  cvmsss2  35960  neibastop2lem  37070  tailf  37085  pibt2  38260  fin2so  38450  sdclem1  38597  elrfirn  43644  elrfirn2  43645  istopclsd  43649  nacsfix  43661  dnnumch1  43989  inpw  49857