Theorem elfpw 9266

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 3919	. 2 ⊢ (𝐴 ∈ (𝒫 𝐵 ∩ Fin) ↔ (𝐴 ∈ 𝒫 𝐵 ∧ 𝐴 ∈ Fin))
2		elpwg 4559	. . 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 2114   ∩ cin 3902   ⊆ wss 3903  𝒫 cpw 4556  Fincfn 8895

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3444  df-in 3910  df-ss 3920  df-pw 4558

This theorem is referenced by:  bitsinv2  16382  bitsf1ocnv  16383  2ebits  16386  bitsinvp1  16388  sadcaddlem  16396  sadadd2lem  16398  sadadd3  16400  sadaddlem  16405  sadasslem  16409  sadeq  16411  firest  17364  acsfiindd  18488  restfpw  23135  cmpcov2  23346  cmpcovf  23347  cncmp  23348  tgcmp  23357  cmpcld  23358  cmpfi  23364  locfincmp  23482  comppfsc  23488  alexsublem  24000  alexsubALTlem2  24004  alexsubALTlem4  24006  alexsubALT  24007  ptcmplem2  24009  ptcmplem3  24010  ptcmplem5  24012  tsmsfbas  24084  tsmslem1  24085  tsmsgsum  24095  tsmssubm  24099  tsmsres  24100  tsmsf1o  24101  tsmsmhm  24102  tsmsadd  24103  tsmsxplem1  24109  tsmsxplem2  24110  tsmsxp  24111  xrge0gsumle  24790  xrge0tsms  24791  indf1ofs  32958  xrge0tsmsd  33166  mvrsfpw  35719  elmpst  35749  istotbnd3  38019  sstotbnd2  38022  sstotbnd  38023  sstotbnd3  38024  equivtotbnd  38026  totbndbnd  38037  prdstotbnd  38042  isnacs3  43064  pwfi2f1o  43450  hbtlem6  43483