Theorem elfpw 9294

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

Syntax hints:   ↔ wb 208   ∧ wa 399   ∈ wcel 2141   ∩ cin 3903   ⊆ wss 3904  𝒫 cpw 4554  Fincfn 8923

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1562  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3455  df-in 3911  df-ss 3921  df-pw 4556

This theorem is referenced by:  bitsinv2  16460  bitsf1ocnv  16461  2ebits  16464  bitsinvp1  16466  sadcaddlem  16474  sadadd2lem  16476  sadadd3  16478  sadaddlem  16483  sadasslem  16487  sadeq  16489  firest  17444  acsfiindd  18568  restfpw  23219  cmpcov2  23430  cmpcovf  23431  cncmp  23432  tgcmp  23441  cmpcld  23442  cmpfi  23448  locfincmp  23566  comppfsc  23572  alexsublem  24084  alexsubALTlem2  24088  alexsubALTlem4  24090  alexsubALT  24091  ptcmplem2  24093  ptcmplem3  24094  ptcmplem5  24096  tsmsfbas  24168  tsmslem1  24169  tsmsgsum  24179  tsmssubm  24183  tsmsres  24184  tsmsf1o  24185  tsmsmhm  24186  tsmsadd  24187  tsmsxplem1  24193  tsmsxplem2  24194  tsmsxp  24195  xrge0gsumle  24874  xrge0tsms  24875  indf1ofs  33005  xrge0tsmsd  33214  mvrsfpw  35820  elmpst  35850  istotbnd3  38234  sstotbnd2  38237  sstotbnd  38238  sstotbnd3  38239  equivtotbnd  38241  totbndbnd  38252  prdstotbnd  38257  isnacs3  43255  pwfi2f1o  43637  hbtlem6  43670