Theorem elfpw 9299

Description: Membership in a class of finite subsets. (Contributed by Stefan O'Rear, 4-Apr-2015.) (Revised by Mario Carneiro, 22-Aug-2015.)

Assertion

Ref	Expression
elfpw	⊢ (𝐴 ∈ (𝒫 𝐵 ∩ Fin) ↔ (𝐴 ⊆ 𝐵 ∧ 𝐴 ∈ Fin))

Proof of Theorem elfpw

Step	Hyp	Ref	Expression
1		elin 3923	. 2 ⊢ (𝐴 ∈ (𝒫 𝐵 ∩ Fin) ↔ (𝐴 ∈ 𝒫 𝐵 ∧ 𝐴 ∈ Fin))
2		elpwg 4561	. . 3 ⊢ (𝐴 ∈ Fin → (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵))
3	2	pm5.32ri 585	. 2 ⊢ ((𝐴 ∈ 𝒫 𝐵 ∧ 𝐴 ∈ Fin) ↔ (𝐴 ⊆ 𝐵 ∧ 𝐴 ∈ Fin))
4	1, 3	bitri 278	1 ⊢ (𝐴 ∈ (𝒫 𝐵 ∩ Fin) ↔ (𝐴 ⊆ 𝐵 ∧ 𝐴 ∈ Fin))

Syntax hints:   ↔ wb 209   ∧ wa 400   ∈ wcel 2145   ∩ cin 3906   ⊆ wss 3907  𝒫 cpw 4558  Fincfn 8931

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1566  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-in 3914  df-ss 3924  df-pw 4560

This theorem is referenced by:  bitsinv2  16489  bitsf1ocnv  16490  2ebits  16493  bitsinvp1  16495  sadcaddlem  16503  sadadd2lem  16505  sadadd3  16507  sadaddlem  16512  sadasslem  16516  sadeq  16518  firest  17473  acsfiindd  18597  restfpw  23293  cmpcov2  23504  cmpcovf  23505  cncmp  23506  tgcmp  23515  cmpcld  23516  cmpfi  23522  locfincmp  23640  comppfsc  23646  alexsublem  24158  alexsubALTlem2  24162  alexsubALTlem4  24164  alexsubALT  24165  ptcmplem2  24167  ptcmplem3  24168  ptcmplem5  24170  tsmsfbas  24242  tsmslem1  24243  tsmsgsum  24253  tsmssubm  24257  tsmsres  24258  tsmsf1o  24259  tsmsmhm  24260  tsmsadd  24261  tsmsxplem1  24267  tsmsxplem2  24268  tsmsxp  24269  xrge0gsumle  24948  xrge0tsms  24949  indf1ofs  33094  xrge0tsmsd  33301  mvrsfpw  35864  elmpst  35894  istotbnd3  38277  sstotbnd2  38280  sstotbnd  38281  sstotbnd3  38282  equivtotbnd  38284  totbndbnd  38295  prdstotbnd  38300  isnacs3  43298  pwfi2f1o  43680  hbtlem6  43713