Theorem elpw2g 5294

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 4563	. 2 ⊢ (𝐴 ∈ 𝒫 𝐵 → 𝐴 ⊆ 𝐵)
2		ssexg 5280	. . . 4 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → 𝐴 ∈ V)
3		elpwg 4559	. . . . 5 ⊢ (𝐴 ∈ V → (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵))
4	3	biimparc 485	. . . 4 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐴 ∈ V) → 𝐴 ∈ 𝒫 𝐵)
5	2, 4	syldan 603	. . 3 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → 𝐴 ∈ 𝒫 𝐵)
6	5	expcom 419	. 2 ⊢ (𝐵 ∈ 𝑉 → (𝐴 ⊆ 𝐵 → 𝐴 ∈ 𝒫 𝐵))
7	1, 6	impbid2 229	1 ⊢ (𝐵 ∈ 𝑉 → (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∈ wcel 2144  Vcvv 3450   ⊆ wss 3895  𝒫 cpw 4556

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-sep 5248

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-ss 3896  df-in 4091  df-pw 4558

This theorem is used by:  elpw2  5295  rabelpw  5297  difelpw  5314  pw2f1olem  9100  fineqvlem  9257  elfir  9407  r1sscl  9792  tskwe  10031  dfac8alem  10108  acni2  10125  fin1ai  10371  fin2i  10373  fin23lem7  10394  fin23lem11  10395  isfin2-2  10397  fin23lem39  10428  isf34lem1  10450  isf34lem2  10451  isf34lem4  10455  isf34lem5  10456  fin1a2lem12  10489  canthnumlem  10733  tsken  10839  tskss  10843  gruss  10881  ismre  17760  mreintcl  17765  mremre  17774  submre  17775  mrcval  17784  mrccl  17785  mrcun  17796  ismri  17805  acsfiel  17828  isacs1i  17831  catcoppccl  18292  acsdrsel  18717  acsdrscl  18720  acsficl  18721  pmtrval  19665  pmtrrn  19671  istopg  23213  uniopn  23215  iscld  23345  ntrval  23354  clsval  23355  discld  23407  mretopd  23410  neival  23420  isnei  23421  lpval  23457  restdis  23496  ordtbaslem  23506  ordtuni  23508  cndis  23609  tgcmp  23719  hauscmplem  23724  comppfsc  23851  elkgen  23855  xkoopn  23908  elqtop  24016  kqffn  24044  isfbas  24148  filss  24172  snfbas  24185  elfg  24190  ufilss  24224  fixufil  24241  cfinufil  24247  ufinffr  24248  ufilen  24249  fin1aufil  24251  flimclslem  24303  hauspwpwf1  24306  supnfcls  24339  flimfnfcls  24347  ptcmplem1  24371  tsmsfbas  24447  blfvalps  24702  blfps  24725  blf  24726  bcthlem5  25649  minveclem3b  25749  sigaclcuni  34750  sigaclcu2  34752  pwsiga  34762  erdsze2lem2  35969  cvmsval  36031  cvmsss2  36039  neibastop2lem  37148  tailf  37163  pibt2  38341  fin2so  38531  sdclem1  38678  elrfirn  43706  elrfirn2  43707  istopclsd  43711  nacsfix  43723  dnnumch1  44051  inpw  49935