Theorem elpw2g 5303

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 4582	. 2 ⊢ (𝐴 ∈ 𝒫 𝐵 → 𝐴 ⊆ 𝐵)
2		ssexg 5293	. . . 4 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → 𝐴 ∈ V)
3		elpwg 4578	. . . . 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 2108  Vcvv 3459   ⊆ wss 3926  𝒫 cpw 4575

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707  ax-sep 5266

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-rab 3416  df-v 3461  df-in 3933  df-ss 3943  df-pw 4577

This theorem is referenced by:  elpw2  5304  rabelpw  5306  difelpw  5324  pw2f1olem  9090  fineqvlem  9270  elfir  9427  r1sscl  9799  tskwe  9964  dfac8alem  10043  acni2  10060  fin1ai  10307  fin2i  10309  fin23lem7  10330  fin23lem11  10331  isfin2-2  10333  fin23lem39  10364  isf34lem1  10386  isf34lem2  10387  isf34lem4  10391  isf34lem5  10392  fin1a2lem12  10425  canthnumlem  10662  tsken  10768  tskss  10772  gruss  10810  ismre  17602  mreintcl  17607  mremre  17616  submre  17617  mrcval  17622  mrccl  17623  mrcun  17634  ismri  17643  acsfiel  17666  isacs1i  17669  catcoppccl  18130  acsdrsel  18553  acsdrscl  18556  acsficl  18557  pmtrval  19432  pmtrrn  19438  istopg  22833  uniopn  22835  iscld  22965  ntrval  22974  clsval  22975  discld  23027  mretopd  23030  neival  23040  isnei  23041  lpval  23077  restdis  23116  ordtbaslem  23126  ordtuni  23128  cndis  23229  tgcmp  23339  hauscmplem  23344  comppfsc  23470  elkgen  23474  xkoopn  23527  elqtop  23635  kqffn  23663  isfbas  23767  filss  23791  snfbas  23804  elfg  23809  ufilss  23843  fixufil  23860  cfinufil  23866  ufinffr  23867  ufilen  23868  fin1aufil  23870  flimclslem  23922  hauspwpwf1  23925  supnfcls  23958  flimfnfcls  23966  ptcmplem1  23990  tsmsfbas  24066  blfvalps  24322  blfps  24345  blf  24346  bcthlem5  25280  minveclem3b  25380  sigaclcuni  34149  sigaclcu2  34151  pwsiga  34161  erdsze2lem2  35226  cvmsval  35288  cvmsss2  35296  neibastop2lem  36378  tailf  36393  pibt2  37435  fin2so  37631  sdclem1  37767  elrfirn  42718  elrfirn2  42719  istopclsd  42723  nacsfix  42735  dnnumch1  43068  inpw  48803