Theorem elpw2g 5269

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 4555	. 2 ⊢ (𝐴 ∈ 𝒫 𝐵 → 𝐴 ⊆ 𝐵)
2		ssexg 5259	. . . 4 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → 𝐴 ∈ V)
3		elpwg 4551	. . . . 5 ⊢ (𝐴 ∈ V → (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵))
4	3	biimparc 479	. . . 4 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐴 ∈ V) → 𝐴 ∈ 𝒫 𝐵)
5	2, 4	syldan 591	. . 3 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → 𝐴 ∈ 𝒫 𝐵)
6	5	expcom 413	. 2 ⊢ (𝐵 ∈ 𝑉 → (𝐴 ⊆ 𝐵 → 𝐴 ∈ 𝒫 𝐵))
7	1, 6	impbid2 226	1 ⊢ (𝐵 ∈ 𝑉 → (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵))

Syntax hints:   → wi 4   ↔ wb 206   ∈ wcel 2110  Vcvv 3434   ⊆ wss 3900  𝒫 cpw 4548

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2112  ax-9 2120  ax-ext 2702  ax-sep 5232

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1544  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2722  df-clel 2804  df-rab 3394  df-v 3436  df-in 3907  df-ss 3917  df-pw 4550

This theorem is referenced by:  elpw2  5270  rabelpw  5272  difelpw  5290  pw2f1olem  8989  fineqvlem  9145  elfir  9294  r1sscl  9670  tskwe  9835  dfac8alem  9912  acni2  9929  fin1ai  10176  fin2i  10178  fin23lem7  10199  fin23lem11  10200  isfin2-2  10202  fin23lem39  10233  isf34lem1  10255  isf34lem2  10256  isf34lem4  10260  isf34lem5  10261  fin1a2lem12  10294  canthnumlem  10531  tsken  10637  tskss  10641  gruss  10679  ismre  17484  mreintcl  17489  mremre  17498  submre  17499  mrcval  17508  mrccl  17509  mrcun  17520  ismri  17529  acsfiel  17552  isacs1i  17555  catcoppccl  18016  acsdrsel  18441  acsdrscl  18444  acsficl  18445  pmtrval  19356  pmtrrn  19362  istopg  22803  uniopn  22805  iscld  22935  ntrval  22944  clsval  22945  discld  22997  mretopd  23000  neival  23010  isnei  23011  lpval  23047  restdis  23086  ordtbaslem  23096  ordtuni  23098  cndis  23199  tgcmp  23309  hauscmplem  23314  comppfsc  23440  elkgen  23444  xkoopn  23497  elqtop  23605  kqffn  23633  isfbas  23737  filss  23761  snfbas  23774  elfg  23779  ufilss  23813  fixufil  23830  cfinufil  23836  ufinffr  23837  ufilen  23838  fin1aufil  23840  flimclslem  23892  hauspwpwf1  23895  supnfcls  23928  flimfnfcls  23936  ptcmplem1  23960  tsmsfbas  24036  blfvalps  24291  blfps  24314  blf  24315  bcthlem5  25248  minveclem3b  25348  sigaclcuni  34121  sigaclcu2  34123  pwsiga  34133  erdsze2lem2  35216  cvmsval  35278  cvmsss2  35286  neibastop2lem  36373  tailf  36388  pibt2  37430  fin2so  37626  sdclem1  37762  elrfirn  42707  elrfirn2  42708  istopclsd  42712  nacsfix  42724  dnnumch1  43056  inpw  48835