Theorem elfpw 9051

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

Syntax hints:   ↔ wb 205   ∧ wa 395   ∈ wcel 2108   ∩ cin 3882   ⊆ wss 3883  𝒫 cpw 4530  Fincfn 8691

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-in 3890  df-ss 3900  df-pw 4532

This theorem is referenced by:  bitsinv2  16078  bitsf1ocnv  16079  2ebits  16082  bitsinvp1  16084  sadcaddlem  16092  sadadd2lem  16094  sadadd3  16096  sadaddlem  16101  sadasslem  16105  sadeq  16107  firest  17060  acsfiindd  18186  restfpw  22238  cmpcov2  22449  cmpcovf  22450  cncmp  22451  tgcmp  22460  cmpcld  22461  cmpfi  22467  locfincmp  22585  comppfsc  22591  alexsublem  23103  alexsubALTlem2  23107  alexsubALTlem4  23109  alexsubALT  23110  ptcmplem2  23112  ptcmplem3  23113  ptcmplem5  23115  tsmsfbas  23187  tsmslem1  23188  tsmsgsum  23198  tsmssubm  23202  tsmsres  23203  tsmsf1o  23204  tsmsmhm  23205  tsmsadd  23206  tsmsxplem1  23212  tsmsxplem2  23213  tsmsxp  23214  xrge0gsumle  23902  xrge0tsms  23903  xrge0tsmsd  31219  indf1ofs  31894  mvrsfpw  33368  elmpst  33398  istotbnd3  35856  sstotbnd2  35859  sstotbnd  35860  sstotbnd3  35861  equivtotbnd  35863  totbndbnd  35874  prdstotbnd  35879  isnacs3  40448  pwfi2f1o  40837  hbtlem6  40870