Theorem elfpw 9394

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 3967	. 2 ⊢ (𝐴 ∈ (𝒫 𝐵 ∩ Fin) ↔ (𝐴 ∈ 𝒫 𝐵 ∧ 𝐴 ∈ Fin))
2		elpwg 4603	. . 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 3950   ⊆ wss 3951  𝒫 cpw 4600  Fincfn 8985

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-in 3958  df-ss 3968  df-pw 4602

This theorem is referenced by:  bitsinv2  16480  bitsf1ocnv  16481  2ebits  16484  bitsinvp1  16486  sadcaddlem  16494  sadadd2lem  16496  sadadd3  16498  sadaddlem  16503  sadasslem  16507  sadeq  16509  firest  17477  acsfiindd  18598  restfpw  23187  cmpcov2  23398  cmpcovf  23399  cncmp  23400  tgcmp  23409  cmpcld  23410  cmpfi  23416  locfincmp  23534  comppfsc  23540  alexsublem  24052  alexsubALTlem2  24056  alexsubALTlem4  24058  alexsubALT  24059  ptcmplem2  24061  ptcmplem3  24062  ptcmplem5  24064  tsmsfbas  24136  tsmslem1  24137  tsmsgsum  24147  tsmssubm  24151  tsmsres  24152  tsmsf1o  24153  tsmsmhm  24154  tsmsadd  24155  tsmsxplem1  24161  tsmsxplem2  24162  tsmsxp  24163  xrge0gsumle  24855  xrge0tsms  24856  indf1ofs  32851  xrge0tsmsd  33065  mvrsfpw  35511  elmpst  35541  istotbnd3  37778  sstotbnd2  37781  sstotbnd  37782  sstotbnd3  37783  equivtotbnd  37785  totbndbnd  37796  prdstotbnd  37801  isnacs3  42721  pwfi2f1o  43108  hbtlem6  43141