Theorem elfpw 9325

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

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401   ∈ wcel 2145   ∩ cin 3901   ⊆ wss 3902  𝒫 cpw 4560  Fincfn 8956

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3455  df-in 3909  df-ss 3919  df-pw 4562

This theorem is used by:  bitsinv2  16539  bitsf1ocnv  16540  2ebits  16543  bitsinvp1  16545  sadcaddlem  16553  sadadd2lem  16555  sadadd3  16557  sadaddlem  16562  sadasslem  16566  sadeq  16568  firest  17523  acsfiindd  18647  restfpw  23410  cmpcov2  23621  cmpcovf  23622  cncmp  23623  tgcmp  23632  cmpcld  23633  cmpfi  23639  locfincmp  23758  comppfsc  23764  alexsublem  24276  alexsubALTlem2  24280  alexsubALTlem4  24282  alexsubALT  24283  ptcmplem2  24285  ptcmplem3  24286  ptcmplem5  24288  tsmsfbas  24360  tsmslem1  24361  tsmsgsum  24371  tsmssubm  24375  tsmsres  24376  tsmsf1o  24377  tsmsmhm  24378  tsmsadd  24379  tsmsxplem1  24385  tsmsxplem2  24386  tsmsxp  24387  xrge0gsumle  25066  xrge0tsms  25067  indf1ofs  33320  xrge0tsmsd  33521  mvrsfpw  36093  elmpst  36123  istotbnd3  38529  sstotbnd2  38532  sstotbnd  38533  sstotbnd3  38534  equivtotbnd  38536  totbndbnd  38547  prdstotbnd  38552  isnacs3  43563  pwfi2f1o  43945  hbtlem6  43978