Theorem elfpw 9391

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

Syntax hints:   ↔ wb 206   ∧ wa 395   ∈ wcel 2105   ∩ cin 3961   ⊆ wss 3962  𝒫 cpw 4604  Fincfn 8983

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-v 3479  df-in 3969  df-ss 3979  df-pw 4606

This theorem is referenced by:  bitsinv2  16476  bitsf1ocnv  16477  2ebits  16480  bitsinvp1  16482  sadcaddlem  16490  sadadd2lem  16492  sadadd3  16494  sadaddlem  16499  sadasslem  16503  sadeq  16505  firest  17478  acsfiindd  18610  restfpw  23202  cmpcov2  23413  cmpcovf  23414  cncmp  23415  tgcmp  23424  cmpcld  23425  cmpfi  23431  locfincmp  23549  comppfsc  23555  alexsublem  24067  alexsubALTlem2  24071  alexsubALTlem4  24073  alexsubALT  24074  ptcmplem2  24076  ptcmplem3  24077  ptcmplem5  24079  tsmsfbas  24151  tsmslem1  24152  tsmsgsum  24162  tsmssubm  24166  tsmsres  24167  tsmsf1o  24168  tsmsmhm  24169  tsmsadd  24170  tsmsxplem1  24176  tsmsxplem2  24177  tsmsxp  24178  xrge0gsumle  24868  xrge0tsms  24869  xrge0tsmsd  33047  indf1ofs  34006  mvrsfpw  35490  elmpst  35520  istotbnd3  37757  sstotbnd2  37760  sstotbnd  37761  sstotbnd3  37762  equivtotbnd  37764  totbndbnd  37775  prdstotbnd  37780  isnacs3  42697  pwfi2f1o  43084  hbtlem6  43117