Theorem elfpw 9305

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 3930	. 2 ⊢ (𝐴 ∈ (𝒫 𝐵 ∩ Fin) ↔ (𝐴 ∈ 𝒫 𝐵 ∧ 𝐴 ∈ Fin))
2		elpwg 4566	. . 3 ⊢ (𝐴 ∈ Fin → (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵))
3	2	pm5.32ri 575	. 2 ⊢ ((𝐴 ∈ 𝒫 𝐵 ∧ 𝐴 ∈ Fin) ↔ (𝐴 ⊆ 𝐵 ∧ 𝐴 ∈ Fin))
4	1, 3	bitri 275	1 ⊢ (𝐴 ∈ (𝒫 𝐵 ∩ Fin) ↔ (𝐴 ⊆ 𝐵 ∧ 𝐴 ∈ Fin))

Syntax hints:   ↔ wb 206   ∧ wa 395   ∈ wcel 2109   ∩ cin 3913   ⊆ wss 3914  𝒫 cpw 4563  Fincfn 8918

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3449  df-in 3921  df-ss 3931  df-pw 4565

This theorem is referenced by:  bitsinv2  16413  bitsf1ocnv  16414  2ebits  16417  bitsinvp1  16419  sadcaddlem  16427  sadadd2lem  16429  sadadd3  16431  sadaddlem  16436  sadasslem  16440  sadeq  16442  firest  17395  acsfiindd  18512  restfpw  23066  cmpcov2  23277  cmpcovf  23278  cncmp  23279  tgcmp  23288  cmpcld  23289  cmpfi  23295  locfincmp  23413  comppfsc  23419  alexsublem  23931  alexsubALTlem2  23935  alexsubALTlem4  23937  alexsubALT  23938  ptcmplem2  23940  ptcmplem3  23941  ptcmplem5  23943  tsmsfbas  24015  tsmslem1  24016  tsmsgsum  24026  tsmssubm  24030  tsmsres  24031  tsmsf1o  24032  tsmsmhm  24033  tsmsadd  24034  tsmsxplem1  24040  tsmsxplem2  24041  tsmsxp  24042  xrge0gsumle  24722  xrge0tsms  24723  indf1ofs  32789  xrge0tsmsd  33002  mvrsfpw  35493  elmpst  35523  istotbnd3  37765  sstotbnd2  37768  sstotbnd  37769  sstotbnd3  37770  equivtotbnd  37772  totbndbnd  37783  prdstotbnd  37788  isnacs3  42698  pwfi2f1o  43085  hbtlem6  43118