Theorem elpw2g 5344

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 4609	. 2 ⊢ (𝐴 ∈ 𝒫 𝐵 → 𝐴 ⊆ 𝐵)
2		ssexg 5323	. . . 4 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → 𝐴 ∈ V)
3		elpwg 4605	. . . . 5 ⊢ (𝐴 ∈ V → (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵))
4	3	biimparc 480	. . . 4 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐴 ∈ V) → 𝐴 ∈ 𝒫 𝐵)
5	2, 4	syldan 591	. . 3 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → 𝐴 ∈ 𝒫 𝐵)
6	5	expcom 414	. 2 ⊢ (𝐵 ∈ 𝑉 → (𝐴 ⊆ 𝐵 → 𝐴 ∈ 𝒫 𝐵))
7	1, 6	impbid2 225	1 ⊢ (𝐵 ∈ 𝑉 → (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵))

Syntax hints:   → wi 4   ↔ wb 205   ∈ wcel 2106  Vcvv 3474   ⊆ wss 3948  𝒫 cpw 4602

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703  ax-sep 5299

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-rab 3433  df-v 3476  df-in 3955  df-ss 3965  df-pw 4604

This theorem is referenced by:  elpw2  5345  elpwi2OLD  5347  pwnss  5349  difelpw  5351  rabelpw  5352  pw2f1olem  9075  fineqvlem  9261  elfir  9409  r1sscl  9779  tskwe  9944  dfac8alem  10023  acni2  10040  fin1ai  10287  fin2i  10289  fin23lem7  10310  fin23lem11  10311  isfin2-2  10313  fin23lem39  10344  isf34lem1  10366  isf34lem2  10367  isf34lem4  10371  isf34lem5  10372  fin1a2lem12  10405  canthnumlem  10642  tsken  10748  tskss  10752  gruss  10790  ismre  17533  mreintcl  17538  mremre  17547  submre  17548  mrcval  17553  mrccl  17554  mrcun  17565  ismri  17574  acsfiel  17597  isacs1i  17600  catcoppccl  18066  catcoppcclOLD  18067  acsdrsel  18495  acsdrscl  18498  acsficl  18499  pmtrval  19318  pmtrrn  19324  istopg  22396  uniopn  22398  iscld  22530  ntrval  22539  clsval  22540  discld  22592  mretopd  22595  neival  22605  isnei  22606  lpval  22642  restdis  22681  ordtbaslem  22691  ordtuni  22693  cndis  22794  tgcmp  22904  hauscmplem  22909  comppfsc  23035  elkgen  23039  xkoopn  23092  elqtop  23200  kqffn  23228  isfbas  23332  filss  23356  snfbas  23369  elfg  23374  ufilss  23408  fixufil  23425  cfinufil  23431  ufinffr  23432  ufilen  23433  fin1aufil  23435  flimclslem  23487  hauspwpwf1  23490  supnfcls  23523  flimfnfcls  23531  ptcmplem1  23555  tsmsfbas  23631  blfvalps  23888  blfps  23911  blf  23912  bcthlem5  24844  minveclem3b  24944  sigaclcuni  33111  sigaclcu2  33113  pwsiga  33123  erdsze2lem2  34190  cvmsval  34252  cvmsss2  34260  neibastop2lem  35240  tailf  35255  pibt2  36293  fin2so  36470  sdclem1  36606  elrfirn  41423  elrfirn2  41424  istopclsd  41428  nacsfix  41440  dnnumch1  41776  inpw  47493