Theorem elpw2g 5264

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 5254	. . . 4 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → 𝐴 ∈ V)
3		elpwg 4535	. . . . 5 ⊢ (𝐴 ∈ V → (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵))
4	3	biimparc 481	. . . 4 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐴 ∈ V) → 𝐴 ∈ 𝒫 𝐵)
5	2, 4	syldan 598	. . 3 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → 𝐴 ∈ 𝒫 𝐵)
6	5	expcom 415	. 2 ⊢ (𝐵 ∈ 𝑉 → (𝐴 ⊆ 𝐵 → 𝐴 ∈ 𝒫 𝐵))
7	1, 6	impbid2 228	1 ⊢ (𝐵 ∈ 𝑉 → (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵))

Syntax hints:   → wi 4   ↔ wb 208   ∈ wcel 2121  Vcvv 3433   ⊆ wss 3885  𝒫 cpw 4532

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713  ax-sep 5221

This theorem depends on definitions:  df-bi 209  df-an 398  df-3an 1095  df-tru 1551  df-ex 1788  df-sb 2075  df-clab 2720  df-cleq 2733  df-clel 2816  df-rab 3394  df-v 3435  df-in 3892  df-ss 3902  df-pw 4534

This theorem is referenced by:  elpw2  5265  rabelpw  5267  difelpw  5285  pw2f1olem  9013  fineqvlem  9170  elfir  9322  r1sscl  9704  tskwe  9869  dfac8alem  9946  acni2  9963  fin1ai  10210  fin2i  10212  fin23lem7  10233  fin23lem11  10234  isfin2-2  10236  fin23lem39  10267  isf34lem1  10289  isf34lem2  10290  isf34lem4  10294  isf34lem5  10295  fin1a2lem12  10328  canthnumlem  10566  tsken  10672  tskss  10676  gruss  10714  ismre  17547  mreintcl  17552  mremre  17561  submre  17562  mrcval  17571  mrccl  17572  mrcun  17583  ismri  17592  acsfiel  17615  isacs1i  17618  catcoppccl  18079  acsdrsel  18504  acsdrscl  18507  acsficl  18508  pmtrval  19421  pmtrrn  19427  istopg  22882  uniopn  22884  iscld  23014  ntrval  23023  clsval  23024  discld  23076  mretopd  23079  neival  23089  isnei  23090  lpval  23126  restdis  23165  ordtbaslem  23175  ordtuni  23177  cndis  23278  tgcmp  23388  hauscmplem  23393  comppfsc  23519  elkgen  23523  xkoopn  23576  elqtop  23684  kqffn  23712  isfbas  23816  filss  23840  snfbas  23853  elfg  23858  ufilss  23892  fixufil  23909  cfinufil  23915  ufinffr  23916  ufilen  23917  fin1aufil  23919  flimclslem  23971  hauspwpwf1  23974  supnfcls  24007  flimfnfcls  24015  ptcmplem1  24039  tsmsfbas  24115  blfvalps  24370  blfps  24393  blf  24394  bcthlem5  25317  minveclem3b  25417  sigaclcuni  34314  sigaclcu2  34316  pwsiga  34326  erdsze2lem2  35447  cvmsval  35509  cvmsss2  35517  neibastop2lem  36603  tailf  36618  pibt2  37794  fin2so  37989  sdclem1  38125  elrfirn  43159  elrfirn2  43160  istopclsd  43164  nacsfix  43176  dnnumch1  43504  inpw  49329