Theorem elfpw 9121

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 3903	. 2 ⊢ (𝐴 ∈ (𝒫 𝐵 ∩ Fin) ↔ (𝐴 ∈ 𝒫 𝐵 ∧ 𝐴 ∈ Fin))
2		elpwg 4536	. . 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 3886   ⊆ wss 3887  𝒫 cpw 4533  Fincfn 8733

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3434  df-in 3894  df-ss 3904  df-pw 4535

This theorem is referenced by:  bitsinv2  16150  bitsf1ocnv  16151  2ebits  16154  bitsinvp1  16156  sadcaddlem  16164  sadadd2lem  16166  sadadd3  16168  sadaddlem  16173  sadasslem  16177  sadeq  16179  firest  17143  acsfiindd  18271  restfpw  22330  cmpcov2  22541  cmpcovf  22542  cncmp  22543  tgcmp  22552  cmpcld  22553  cmpfi  22559  locfincmp  22677  comppfsc  22683  alexsublem  23195  alexsubALTlem2  23199  alexsubALTlem4  23201  alexsubALT  23202  ptcmplem2  23204  ptcmplem3  23205  ptcmplem5  23207  tsmsfbas  23279  tsmslem1  23280  tsmsgsum  23290  tsmssubm  23294  tsmsres  23295  tsmsf1o  23296  tsmsmhm  23297  tsmsadd  23298  tsmsxplem1  23304  tsmsxplem2  23305  tsmsxp  23306  xrge0gsumle  23996  xrge0tsms  23997  xrge0tsmsd  31317  indf1ofs  31994  mvrsfpw  33468  elmpst  33498  istotbnd3  35929  sstotbnd2  35932  sstotbnd  35933  sstotbnd3  35934  equivtotbnd  35936  totbndbnd  35947  prdstotbnd  35952  isnacs3  40532  pwfi2f1o  40921  hbtlem6  40954