Theorem elfpw 8826

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

Syntax hints:   ↔ wb 208   ∧ wa 398   ∈ wcel 2114   ∩ cin 3935   ⊆ wss 3936  𝒫 cpw 4539  Fincfn 8509

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-v 3496  df-in 3943  df-ss 3952  df-pw 4541

This theorem is referenced by:  bitsinv2  15792  bitsf1ocnv  15793  2ebits  15796  bitsinvp1  15798  sadcaddlem  15806  sadadd2lem  15808  sadadd3  15810  sadaddlem  15815  sadasslem  15819  sadeq  15821  firest  16706  acsfiindd  17787  restfpw  21787  cmpcov2  21998  cmpcovf  21999  cncmp  22000  tgcmp  22009  cmpcld  22010  cmpfi  22016  locfincmp  22134  comppfsc  22140  alexsublem  22652  alexsubALTlem2  22656  alexsubALTlem4  22658  alexsubALT  22659  ptcmplem2  22661  ptcmplem3  22662  ptcmplem5  22664  tsmsfbas  22736  tsmslem1  22737  tsmsgsum  22747  tsmssubm  22751  tsmsres  22752  tsmsf1o  22753  tsmsmhm  22754  tsmsadd  22755  tsmsxplem1  22761  tsmsxplem2  22762  tsmsxp  22763  xrge0gsumle  23441  xrge0tsms  23442  xrge0tsmsd  30692  indf1ofs  31285  mvrsfpw  32753  elmpst  32783  istotbnd3  35064  sstotbnd2  35067  sstotbnd  35068  sstotbnd3  35069  equivtotbnd  35071  totbndbnd  35082  prdstotbnd  35087  isnacs3  39327  pwfi2f1o  39716  hbtlem6  39749