Theorem elfpw 9254

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 3917	. 2 ⊢ (𝐴 ∈ (𝒫 𝐵 ∩ Fin) ↔ (𝐴 ∈ 𝒫 𝐵 ∧ 𝐴 ∈ Fin))
2		elpwg 4557	. . 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 2113   ∩ cin 3900   ⊆ wss 3901  𝒫 cpw 4554  Fincfn 8883

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 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-in 3908  df-ss 3918  df-pw 4556

This theorem is referenced by:  bitsinv2  16370  bitsf1ocnv  16371  2ebits  16374  bitsinvp1  16376  sadcaddlem  16384  sadadd2lem  16386  sadadd3  16388  sadaddlem  16393  sadasslem  16397  sadeq  16399  firest  17352  acsfiindd  18476  restfpw  23123  cmpcov2  23334  cmpcovf  23335  cncmp  23336  tgcmp  23345  cmpcld  23346  cmpfi  23352  locfincmp  23470  comppfsc  23476  alexsublem  23988  alexsubALTlem2  23992  alexsubALTlem4  23994  alexsubALT  23995  ptcmplem2  23997  ptcmplem3  23998  ptcmplem5  24000  tsmsfbas  24072  tsmslem1  24073  tsmsgsum  24083  tsmssubm  24087  tsmsres  24088  tsmsf1o  24089  tsmsmhm  24090  tsmsadd  24091  tsmsxplem1  24097  tsmsxplem2  24098  tsmsxp  24099  xrge0gsumle  24778  xrge0tsms  24779  indf1ofs  32948  xrge0tsmsd  33155  mvrsfpw  35700  elmpst  35730  istotbnd3  37972  sstotbnd2  37975  sstotbnd  37976  sstotbnd3  37977  equivtotbnd  37979  totbndbnd  37990  prdstotbnd  37995  isnacs3  42952  pwfi2f1o  43338  hbtlem6  43371