Theorem elfpw 9374

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

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401   ∈ wcel 2147   ⊆ wss 3900   ∩ cin 4092  𝒫 cpw 4560  Fincfn 9004

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-ss 3901  df-in 4094  df-pw 4562

This theorem is used by:  bitsinv2  16645  bitsf1ocnv  16646  2ebits  16649  bitsinvp1  16651  sadcaddlem  16659  sadadd2lem  16661  sadadd3  16663  sadaddlem  16668  sadasslem  16672  sadeq  16674  firest  17635  acsfiindd  18759  restfpw  23530  cmpcov2  23741  cmpcovf  23742  cncmp  23743  tgcmp  23752  cmpcld  23753  cmpfi  23759  locfincmp  23878  comppfsc  23884  alexsublem  24396  alexsubALTlem2  24400  alexsubALTlem4  24402  alexsubALT  24403  ptcmplem2  24405  ptcmplem3  24406  ptcmplem5  24408  tsmsfbas  24480  tsmslem1  24481  tsmsgsum  24491  tsmssubm  24495  tsmsres  24496  tsmsf1o  24497  tsmsmhm  24498  tsmsadd  24499  tsmsxplem1  24505  tsmsxplem2  24506  tsmsxp  24507  xrge0gsumle  25186  xrge0tsms  25187  indf1ofs  33506  xrge0tsmsd  33710  mvrsfpw  36451  elmpst  36481  istotbnd3  38908  sstotbnd2  38911  sstotbnd  38912  sstotbnd3  38913  equivtotbnd  38915  totbndbnd  38926  prdstotbnd  38931  isnacs3  43925  pwfi2f1o  44302  hbtlem6  44334