Theorem elfpw 8151

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

Syntax hints:   ↔ wb 195   ∧ wa 383   ∈ wcel 1977   ∩ cin 3539   ⊆ wss 3540  𝒫 cpw 4108  Fincfn 7841

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-in 3547  df-ss 3554  df-pw 4110

This theorem is referenced by:  bitsinv2  15003  bitsf1ocnv  15004  2ebits  15007  bitsinvp1  15009  sadcaddlem  15017  sadadd2lem  15019  sadadd3  15021  sadaddlem  15026  sadasslem  15030  sadeq  15032  firest  15916  acsfiindd  17000  restfpw  20793  cmpcov2  21003  cmpcovf  21004  cncmp  21005  tgcmp  21014  cmpcld  21015  cmpfi  21021  locfincmp  21139  comppfsc  21145  alexsublem  21658  alexsubALTlem2  21662  alexsubALTlem4  21664  alexsubALT  21665  ptcmplem2  21667  ptcmplem3  21668  ptcmplem5  21670  tsmsfbas  21741  tsmslem1  21742  tsmsgsum  21752  tsmssubm  21756  tsmsres  21757  tsmsf1o  21758  tsmsmhm  21759  tsmsadd  21760  tsmsxplem1  21766  tsmsxplem2  21767  tsmsxp  21768  xrge0gsumle  22444  xrge0tsms  22445  xrge0tsmsd  29116  indf1ofs  29415  mvrsfpw  30657  elmpst  30687  istotbnd3  32740  sstotbnd2  32743  sstotbnd  32744  sstotbnd3  32745  equivtotbnd  32747  totbndbnd  32758  prdstotbnd  32763  isnacs3  36291  pwfi2f1o  36684  hbtlem6  36718