Theorem elfpw 9424

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 3992	. 2 ⊢ (𝐴 ∈ (𝒫 𝐵 ∩ Fin) ↔ (𝐴 ∈ 𝒫 𝐵 ∧ 𝐴 ∈ Fin))
2		elpwg 4625	. . 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 2108   ∩ cin 3975   ⊆ wss 3976  𝒫 cpw 4622  Fincfn 9003

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-in 3983  df-ss 3993  df-pw 4624

This theorem is referenced by:  bitsinv2  16489  bitsf1ocnv  16490  2ebits  16493  bitsinvp1  16495  sadcaddlem  16503  sadadd2lem  16505  sadadd3  16507  sadaddlem  16512  sadasslem  16516  sadeq  16518  firest  17492  acsfiindd  18623  restfpw  23208  cmpcov2  23419  cmpcovf  23420  cncmp  23421  tgcmp  23430  cmpcld  23431  cmpfi  23437  locfincmp  23555  comppfsc  23561  alexsublem  24073  alexsubALTlem2  24077  alexsubALTlem4  24079  alexsubALT  24080  ptcmplem2  24082  ptcmplem3  24083  ptcmplem5  24085  tsmsfbas  24157  tsmslem1  24158  tsmsgsum  24168  tsmssubm  24172  tsmsres  24173  tsmsf1o  24174  tsmsmhm  24175  tsmsadd  24176  tsmsxplem1  24182  tsmsxplem2  24183  tsmsxp  24184  xrge0gsumle  24874  xrge0tsms  24875  xrge0tsmsd  33041  indf1ofs  33990  mvrsfpw  35474  elmpst  35504  istotbnd3  37731  sstotbnd2  37734  sstotbnd  37735  sstotbnd3  37736  equivtotbnd  37738  totbndbnd  37749  prdstotbnd  37754  isnacs3  42666  pwfi2f1o  43053  hbtlem6  43086