Theorem elfpw 8829

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 4172	. 2 ⊢ (𝐴 ∈ (𝒫 𝐵 ∩ Fin) ↔ (𝐴 ∈ 𝒫 𝐵 ∧ 𝐴 ∈ Fin))
2		elpwg 4545	. . 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 2113   ∩ cin 3938   ⊆ wss 3939  𝒫 cpw 4542  Fincfn 8512

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2160  ax-12 2176  ax-ext 2796

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1539  df-ex 1780  df-nf 1784  df-sb 2069  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2966  df-v 3499  df-in 3946  df-ss 3955  df-pw 4544

This theorem is referenced by:  bitsinv2  15795  bitsf1ocnv  15796  2ebits  15799  bitsinvp1  15801  sadcaddlem  15809  sadadd2lem  15811  sadadd3  15813  sadaddlem  15818  sadasslem  15822  sadeq  15824  firest  16709  acsfiindd  17790  restfpw  21790  cmpcov2  22001  cmpcovf  22002  cncmp  22003  tgcmp  22012  cmpcld  22013  cmpfi  22019  locfincmp  22137  comppfsc  22143  alexsublem  22655  alexsubALTlem2  22659  alexsubALTlem4  22661  alexsubALT  22662  ptcmplem2  22664  ptcmplem3  22665  ptcmplem5  22667  tsmsfbas  22739  tsmslem1  22740  tsmsgsum  22750  tsmssubm  22754  tsmsres  22755  tsmsf1o  22756  tsmsmhm  22757  tsmsadd  22758  tsmsxplem1  22764  tsmsxplem2  22765  tsmsxp  22766  xrge0gsumle  23444  xrge0tsms  23445  xrge0tsmsd  30696  indf1ofs  31289  mvrsfpw  32757  elmpst  32787  istotbnd3  35053  sstotbnd2  35056  sstotbnd  35057  sstotbnd3  35058  equivtotbnd  35060  totbndbnd  35071  prdstotbnd  35076  isnacs3  39313  pwfi2f1o  39702  hbtlem6  39735