Theorem elfpw 9312

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 3933	. 2 ⊢ (𝐴 ∈ (𝒫 𝐵 ∩ Fin) ↔ (𝐴 ∈ 𝒫 𝐵 ∧ 𝐴 ∈ Fin))
2		elpwg 4569	. . 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 3916   ⊆ wss 3917  𝒫 cpw 4566  Fincfn 8921

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 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-v 3452  df-in 3924  df-ss 3934  df-pw 4568

This theorem is referenced by:  bitsinv2  16420  bitsf1ocnv  16421  2ebits  16424  bitsinvp1  16426  sadcaddlem  16434  sadadd2lem  16436  sadadd3  16438  sadaddlem  16443  sadasslem  16447  sadeq  16449  firest  17402  acsfiindd  18519  restfpw  23073  cmpcov2  23284  cmpcovf  23285  cncmp  23286  tgcmp  23295  cmpcld  23296  cmpfi  23302  locfincmp  23420  comppfsc  23426  alexsublem  23938  alexsubALTlem2  23942  alexsubALTlem4  23944  alexsubALT  23945  ptcmplem2  23947  ptcmplem3  23948  ptcmplem5  23950  tsmsfbas  24022  tsmslem1  24023  tsmsgsum  24033  tsmssubm  24037  tsmsres  24038  tsmsf1o  24039  tsmsmhm  24040  tsmsadd  24041  tsmsxplem1  24047  tsmsxplem2  24048  tsmsxp  24049  xrge0gsumle  24729  xrge0tsms  24730  indf1ofs  32796  xrge0tsmsd  33009  mvrsfpw  35500  elmpst  35530  istotbnd3  37772  sstotbnd2  37775  sstotbnd  37776  sstotbnd3  37777  equivtotbnd  37779  totbndbnd  37790  prdstotbnd  37795  isnacs3  42705  pwfi2f1o  43092  hbtlem6  43125