Theorem elfpw 9263

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 3921	. 2 ⊢ (𝐴 ∈ (𝒫 𝐵 ∩ Fin) ↔ (𝐴 ∈ 𝒫 𝐵 ∧ 𝐴 ∈ Fin))
2		elpwg 4556	. . 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 2109   ∩ cin 3904   ⊆ wss 3905  𝒫 cpw 4553  Fincfn 8879

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3440  df-in 3912  df-ss 3922  df-pw 4555

This theorem is referenced by:  bitsinv2  16372  bitsf1ocnv  16373  2ebits  16376  bitsinvp1  16378  sadcaddlem  16386  sadadd2lem  16388  sadadd3  16390  sadaddlem  16395  sadasslem  16399  sadeq  16401  firest  17354  acsfiindd  18477  restfpw  23082  cmpcov2  23293  cmpcovf  23294  cncmp  23295  tgcmp  23304  cmpcld  23305  cmpfi  23311  locfincmp  23429  comppfsc  23435  alexsublem  23947  alexsubALTlem2  23951  alexsubALTlem4  23953  alexsubALT  23954  ptcmplem2  23956  ptcmplem3  23957  ptcmplem5  23959  tsmsfbas  24031  tsmslem1  24032  tsmsgsum  24042  tsmssubm  24046  tsmsres  24047  tsmsf1o  24048  tsmsmhm  24049  tsmsadd  24050  tsmsxplem1  24056  tsmsxplem2  24057  tsmsxp  24058  xrge0gsumle  24738  xrge0tsms  24739  indf1ofs  32822  xrge0tsmsd  33028  mvrsfpw  35481  elmpst  35511  istotbnd3  37753  sstotbnd2  37756  sstotbnd  37757  sstotbnd3  37758  equivtotbnd  37760  totbndbnd  37771  prdstotbnd  37776  isnacs3  42686  pwfi2f1o  43072  hbtlem6  43105