Theorem elfpw 9097

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

Syntax hints:   ↔ wb 205   ∧ wa 396   ∈ wcel 2110   ∩ cin 3891   ⊆ wss 3892  𝒫 cpw 4539  Fincfn 8714

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-8 2112  ax-9 2120  ax-ext 2711

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1545  df-ex 1787  df-sb 2072  df-clab 2718  df-cleq 2732  df-clel 2818  df-v 3433  df-in 3899  df-ss 3909  df-pw 4541

This theorem is referenced by:  bitsinv2  16146  bitsf1ocnv  16147  2ebits  16150  bitsinvp1  16152  sadcaddlem  16160  sadadd2lem  16162  sadadd3  16164  sadaddlem  16169  sadasslem  16173  sadeq  16175  firest  17139  acsfiindd  18267  restfpw  22326  cmpcov2  22537  cmpcovf  22538  cncmp  22539  tgcmp  22548  cmpcld  22549  cmpfi  22555  locfincmp  22673  comppfsc  22679  alexsublem  23191  alexsubALTlem2  23195  alexsubALTlem4  23197  alexsubALT  23198  ptcmplem2  23200  ptcmplem3  23201  ptcmplem5  23203  tsmsfbas  23275  tsmslem1  23276  tsmsgsum  23286  tsmssubm  23290  tsmsres  23291  tsmsf1o  23292  tsmsmhm  23293  tsmsadd  23294  tsmsxplem1  23300  tsmsxplem2  23301  tsmsxp  23302  xrge0gsumle  23992  xrge0tsms  23993  xrge0tsmsd  31311  indf1ofs  31988  mvrsfpw  33462  elmpst  33492  istotbnd3  35923  sstotbnd2  35926  sstotbnd  35927  sstotbnd3  35928  equivtotbnd  35930  totbndbnd  35941  prdstotbnd  35946  isnacs3  40527  pwfi2f1o  40916  hbtlem6  40949