Theorem elfpw 9391

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 3962	. 2 ⊢ (𝐴 ∈ (𝒫 𝐵 ∩ Fin) ↔ (𝐴 ∈ 𝒫 𝐵 ∧ 𝐴 ∈ Fin))
2		elpwg 4600	. . 3 ⊢ (𝐴 ∈ Fin → (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵))
3	2	pm5.32ri 574	. 2 ⊢ ((𝐴 ∈ 𝒫 𝐵 ∧ 𝐴 ∈ Fin) ↔ (𝐴 ⊆ 𝐵 ∧ 𝐴 ∈ Fin))
4	1, 3	bitri 274	1 ⊢ (𝐴 ∈ (𝒫 𝐵 ∩ Fin) ↔ (𝐴 ⊆ 𝐵 ∧ 𝐴 ∈ Fin))

Syntax hints:   ↔ wb 205   ∧ wa 394   ∈ wcel 2099   ∩ cin 3945   ⊆ wss 3946  𝒫 cpw 4597  Fincfn 8966

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2697

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2704  df-cleq 2718  df-clel 2803  df-v 3464  df-in 3953  df-ss 3963  df-pw 4599

This theorem is referenced by:  bitsinv2  16438  bitsf1ocnv  16439  2ebits  16442  bitsinvp1  16444  sadcaddlem  16452  sadadd2lem  16454  sadadd3  16456  sadaddlem  16461  sadasslem  16465  sadeq  16467  firest  17442  acsfiindd  18573  restfpw  23171  cmpcov2  23382  cmpcovf  23383  cncmp  23384  tgcmp  23393  cmpcld  23394  cmpfi  23400  locfincmp  23518  comppfsc  23524  alexsublem  24036  alexsubALTlem2  24040  alexsubALTlem4  24042  alexsubALT  24043  ptcmplem2  24045  ptcmplem3  24046  ptcmplem5  24048  tsmsfbas  24120  tsmslem1  24121  tsmsgsum  24131  tsmssubm  24135  tsmsres  24136  tsmsf1o  24137  tsmsmhm  24138  tsmsadd  24139  tsmsxplem1  24145  tsmsxplem2  24146  tsmsxp  24147  xrge0gsumle  24837  xrge0tsms  24838  xrge0tsmsd  32930  indf1ofs  33872  mvrsfpw  35347  elmpst  35377  istotbnd3  37485  sstotbnd2  37488  sstotbnd  37489  sstotbnd3  37490  equivtotbnd  37492  totbndbnd  37503  prdstotbnd  37508  isnacs3  42404  pwfi2f1o  42794  hbtlem6  42827