Theorem elpw2g 5263

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 4539	. 2 ⊢ (𝐴 ∈ 𝒫 𝐵 → 𝐴 ⊆ 𝐵)
2		ssexg 5242	. . . 4 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → 𝐴 ∈ V)
3		elpwg 4533	. . . . 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 2108  Vcvv 3422   ⊆ wss 3883  𝒫 cpw 4530

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709  ax-sep 5218

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072  df-v 3424  df-in 3890  df-ss 3900  df-pw 4532

This theorem is referenced by:  elpw2  5264  elpwi2OLD  5266  pwnss  5267  difelpw  5269  rabelpw  5270  pw2f1olem  8816  fineqvlem  8966  elfir  9104  r1sscl  9474  tskwe  9639  dfac8alem  9716  acni2  9733  fin1ai  9980  fin2i  9982  fin23lem7  10003  fin23lem11  10004  isfin2-2  10006  fin23lem39  10037  isf34lem1  10059  isf34lem2  10060  isf34lem4  10064  isf34lem5  10065  fin1a2lem12  10098  canthnumlem  10335  tsken  10441  tskss  10445  gruss  10483  ismre  17216  mreintcl  17221  mremre  17230  submre  17231  mrcval  17236  mrccl  17237  mrcun  17248  ismri  17257  acsfiel  17280  isacs1i  17283  catcoppccl  17748  catcoppcclOLD  17749  acsdrsel  18176  acsdrscl  18179  acsficl  18180  pmtrval  18974  pmtrrn  18980  istopg  21952  uniopn  21954  iscld  22086  ntrval  22095  clsval  22096  discld  22148  mretopd  22151  neival  22161  isnei  22162  lpval  22198  restdis  22237  ordtbaslem  22247  ordtuni  22249  cndis  22350  tgcmp  22460  hauscmplem  22465  comppfsc  22591  elkgen  22595  xkoopn  22648  elqtop  22756  kqffn  22784  isfbas  22888  filss  22912  snfbas  22925  elfg  22930  ufilss  22964  fixufil  22981  cfinufil  22987  ufinffr  22988  ufilen  22989  fin1aufil  22991  flimclslem  23043  hauspwpwf1  23046  supnfcls  23079  flimfnfcls  23087  ptcmplem1  23111  tsmsfbas  23187  blfvalps  23444  blfps  23467  blf  23468  bcthlem5  24397  minveclem3b  24497  sigaclcuni  31986  sigaclcu2  31988  pwsiga  31998  erdsze2lem2  33066  cvmsval  33128  cvmsss2  33136  neibastop2lem  34476  tailf  34491  pibt2  35515  fin2so  35691  sdclem1  35828  elrfirn  40433  elrfirn2  40434  istopclsd  40438  nacsfix  40450  dnnumch1  40785  inpw  46052