Theorem elfpw 9245

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 3914	. 2 ⊢ (𝐴 ∈ (𝒫 𝐵 ∩ Fin) ↔ (𝐴 ∈ 𝒫 𝐵 ∧ 𝐴 ∈ Fin))
2		elpwg 4552	. . 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 3897   ⊆ wss 3898  𝒫 cpw 4549  Fincfn 8875

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 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-v 3439  df-in 3905  df-ss 3915  df-pw 4551

This theorem is referenced by:  bitsinv2  16356  bitsf1ocnv  16357  2ebits  16360  bitsinvp1  16362  sadcaddlem  16370  sadadd2lem  16372  sadadd3  16374  sadaddlem  16379  sadasslem  16383  sadeq  16385  firest  17338  acsfiindd  18461  restfpw  23095  cmpcov2  23306  cmpcovf  23307  cncmp  23308  tgcmp  23317  cmpcld  23318  cmpfi  23324  locfincmp  23442  comppfsc  23448  alexsublem  23960  alexsubALTlem2  23964  alexsubALTlem4  23966  alexsubALT  23967  ptcmplem2  23969  ptcmplem3  23970  ptcmplem5  23972  tsmsfbas  24044  tsmslem1  24045  tsmsgsum  24055  tsmssubm  24059  tsmsres  24060  tsmsf1o  24061  tsmsmhm  24062  tsmsadd  24063  tsmsxplem1  24069  tsmsxplem2  24070  tsmsxp  24071  xrge0gsumle  24750  xrge0tsms  24751  indf1ofs  32854  xrge0tsmsd  33049  mvrsfpw  35571  elmpst  35601  istotbnd3  37832  sstotbnd2  37835  sstotbnd  37836  sstotbnd3  37837  equivtotbnd  37839  totbndbnd  37850  prdstotbnd  37855  isnacs3  42828  pwfi2f1o  43214  hbtlem6  43247