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

Syntax hints:   ↔ wb 205   ∧ wa 396   ∈ wcel 2106   ∩ cin 3912   ⊆ wss 3913  𝒫 cpw 4565  Fincfn 8890

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-v 3448  df-in 3920  df-ss 3930  df-pw 4567

This theorem is referenced by:  bitsinv2  16334  bitsf1ocnv  16335  2ebits  16338  bitsinvp1  16340  sadcaddlem  16348  sadadd2lem  16350  sadadd3  16352  sadaddlem  16357  sadasslem  16361  sadeq  16363  firest  17328  acsfiindd  18456  restfpw  22567  cmpcov2  22778  cmpcovf  22779  cncmp  22780  tgcmp  22789  cmpcld  22790  cmpfi  22796  locfincmp  22914  comppfsc  22920  alexsublem  23432  alexsubALTlem2  23436  alexsubALTlem4  23438  alexsubALT  23439  ptcmplem2  23441  ptcmplem3  23442  ptcmplem5  23444  tsmsfbas  23516  tsmslem1  23517  tsmsgsum  23527  tsmssubm  23531  tsmsres  23532  tsmsf1o  23533  tsmsmhm  23534  tsmsadd  23535  tsmsxplem1  23541  tsmsxplem2  23542  tsmsxp  23543  xrge0gsumle  24233  xrge0tsms  24234  xrge0tsmsd  31969  indf1ofs  32714  mvrsfpw  34187  elmpst  34217  istotbnd3  36303  sstotbnd2  36306  sstotbnd  36307  sstotbnd3  36308  equivtotbnd  36310  totbndbnd  36321  prdstotbnd  36326  isnacs3  41091  pwfi2f1o  41481  hbtlem6  41514