Theorem elfpw 9257

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 3906	. 2 ⊢ (𝐴 ∈ (𝒫 𝐵 ∩ Fin) ↔ (𝐴 ∈ 𝒫 𝐵 ∧ 𝐴 ∈ Fin))
2		elpwg 4545	. . 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 3889   ⊆ wss 3890  𝒫 cpw 4542  Fincfn 8886

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 3432  df-in 3897  df-ss 3907  df-pw 4544

This theorem is referenced by:  bitsinv2  16403  bitsf1ocnv  16404  2ebits  16407  bitsinvp1  16409  sadcaddlem  16417  sadadd2lem  16419  sadadd3  16421  sadaddlem  16426  sadasslem  16430  sadeq  16432  firest  17386  acsfiindd  18510  restfpw  23154  cmpcov2  23365  cmpcovf  23366  cncmp  23367  tgcmp  23376  cmpcld  23377  cmpfi  23383  locfincmp  23501  comppfsc  23507  alexsublem  24019  alexsubALTlem2  24023  alexsubALTlem4  24025  alexsubALT  24026  ptcmplem2  24028  ptcmplem3  24029  ptcmplem5  24031  tsmsfbas  24103  tsmslem1  24104  tsmsgsum  24114  tsmssubm  24118  tsmsres  24119  tsmsf1o  24120  tsmsmhm  24121  tsmsadd  24122  tsmsxplem1  24128  tsmsxplem2  24129  tsmsxp  24130  xrge0gsumle  24809  xrge0tsms  24810  indf1ofs  32941  xrge0tsmsd  33149  mvrsfpw  35704  elmpst  35734  istotbnd3  38106  sstotbnd2  38109  sstotbnd  38110  sstotbnd3  38111  equivtotbnd  38113  totbndbnd  38124  prdstotbnd  38129  isnacs3  43156  pwfi2f1o  43542  hbtlem6  43575