Theorem elfpw 8810

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

Syntax hints:   ↔ wb 209   ∧ wa 399   ∈ wcel 2111   ∩ cin 3880   ⊆ wss 3881  𝒫 cpw 4497  Fincfn 8492

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-in 3888  df-ss 3898  df-pw 4499

This theorem is referenced by:  bitsinv2  15782  bitsf1ocnv  15783  2ebits  15786  bitsinvp1  15788  sadcaddlem  15796  sadadd2lem  15798  sadadd3  15800  sadaddlem  15805  sadasslem  15809  sadeq  15811  firest  16698  acsfiindd  17779  restfpw  21784  cmpcov2  21995  cmpcovf  21996  cncmp  21997  tgcmp  22006  cmpcld  22007  cmpfi  22013  locfincmp  22131  comppfsc  22137  alexsublem  22649  alexsubALTlem2  22653  alexsubALTlem4  22655  alexsubALT  22656  ptcmplem2  22658  ptcmplem3  22659  ptcmplem5  22661  tsmsfbas  22733  tsmslem1  22734  tsmsgsum  22744  tsmssubm  22748  tsmsres  22749  tsmsf1o  22750  tsmsmhm  22751  tsmsadd  22752  tsmsxplem1  22758  tsmsxplem2  22759  tsmsxp  22760  xrge0gsumle  23438  xrge0tsms  23439  xrge0tsmsd  30742  indf1ofs  31395  mvrsfpw  32866  elmpst  32896  istotbnd3  35209  sstotbnd2  35212  sstotbnd  35213  sstotbnd3  35214  equivtotbnd  35216  totbndbnd  35227  prdstotbnd  35232  isnacs3  39651  pwfi2f1o  40040  hbtlem6  40073