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

Syntax hints:   ↔ wb 209   ∧ wa 400   ∈ wcel 2143   ∩ cin 3905   ⊆ wss 3906  𝒫 cpw 4563  Fincfn 8944

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-in 3913  df-ss 3923  df-pw 4565

This theorem is referenced by:  bitsinv2  16502  bitsf1ocnv  16503  2ebits  16506  bitsinvp1  16508  sadcaddlem  16516  sadadd2lem  16518  sadadd3  16520  sadaddlem  16525  sadasslem  16529  sadeq  16531  firest  17486  acsfiindd  18610  restfpw  23317  cmpcov2  23528  cmpcovf  23529  cncmp  23530  tgcmp  23539  cmpcld  23540  cmpfi  23546  locfincmp  23664  comppfsc  23670  alexsublem  24182  alexsubALTlem2  24186  alexsubALTlem4  24188  alexsubALT  24189  ptcmplem2  24191  ptcmplem3  24192  ptcmplem5  24194  tsmsfbas  24266  tsmslem1  24267  tsmsgsum  24277  tsmssubm  24281  tsmsres  24282  tsmsf1o  24283  tsmsmhm  24284  tsmsadd  24285  tsmsxplem1  24291  tsmsxplem2  24292  tsmsxp  24293  xrge0gsumle  24972  xrge0tsms  24973  indf1ofs  33167  xrge0tsmsd  33374  mvrsfpw  35979  elmpst  36009  istotbnd3  38403  sstotbnd2  38406  sstotbnd  38407  sstotbnd3  38408  equivtotbnd  38410  totbndbnd  38421  prdstotbnd  38426  isnacs3  43424  pwfi2f1o  43806  hbtlem6  43839