Theorem elfpw 9366

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 3942	. 2 ⊢ (𝐴 ∈ (𝒫 𝐵 ∩ Fin) ↔ (𝐴 ∈ 𝒫 𝐵 ∧ 𝐴 ∈ Fin))
2		elpwg 4578	. . 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 3925   ⊆ wss 3926  𝒫 cpw 4575  Fincfn 8959

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-v 3461  df-in 3933  df-ss 3943  df-pw 4577

This theorem is referenced by:  bitsinv2  16462  bitsf1ocnv  16463  2ebits  16466  bitsinvp1  16468  sadcaddlem  16476  sadadd2lem  16478  sadadd3  16480  sadaddlem  16485  sadasslem  16489  sadeq  16491  firest  17446  acsfiindd  18563  restfpw  23117  cmpcov2  23328  cmpcovf  23329  cncmp  23330  tgcmp  23339  cmpcld  23340  cmpfi  23346  locfincmp  23464  comppfsc  23470  alexsublem  23982  alexsubALTlem2  23986  alexsubALTlem4  23988  alexsubALT  23989  ptcmplem2  23991  ptcmplem3  23992  ptcmplem5  23994  tsmsfbas  24066  tsmslem1  24067  tsmsgsum  24077  tsmssubm  24081  tsmsres  24082  tsmsf1o  24083  tsmsmhm  24084  tsmsadd  24085  tsmsxplem1  24091  tsmsxplem2  24092  tsmsxp  24093  xrge0gsumle  24773  xrge0tsms  24774  indf1ofs  32843  xrge0tsmsd  33056  mvrsfpw  35528  elmpst  35558  istotbnd3  37795  sstotbnd2  37798  sstotbnd  37799  sstotbnd3  37800  equivtotbnd  37802  totbndbnd  37813  prdstotbnd  37818  isnacs3  42733  pwfi2f1o  43120  hbtlem6  43153