Theorem elfpw 9238

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 3918	. 2 ⊢ (𝐴 ∈ (𝒫 𝐵 ∩ Fin) ↔ (𝐴 ∈ 𝒫 𝐵 ∧ 𝐴 ∈ Fin))
2		elpwg 4553	. . 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 2111   ∩ cin 3901   ⊆ wss 3902  𝒫 cpw 4550  Fincfn 8869

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-in 3909  df-ss 3919  df-pw 4552

This theorem is referenced by:  bitsinv2  16354  bitsf1ocnv  16355  2ebits  16358  bitsinvp1  16360  sadcaddlem  16368  sadadd2lem  16370  sadadd3  16372  sadaddlem  16377  sadasslem  16381  sadeq  16383  firest  17336  acsfiindd  18459  restfpw  23095  cmpcov2  23306  cmpcovf  23307  cncmp  23308  tgcmp  23317  cmpcld  23318  cmpfi  23324  locfincmp  23442  comppfsc  23448  alexsublem  23960  alexsubALTlem2  23964  alexsubALTlem4  23966  alexsubALT  23967  ptcmplem2  23969  ptcmplem3  23970  ptcmplem5  23972  tsmsfbas  24044  tsmslem1  24045  tsmsgsum  24055  tsmssubm  24059  tsmsres  24060  tsmsf1o  24061  tsmsmhm  24062  tsmsadd  24063  tsmsxplem1  24069  tsmsxplem2  24070  tsmsxp  24071  xrge0gsumle  24750  xrge0tsms  24751  indf1ofs  32845  xrge0tsmsd  33040  mvrsfpw  35548  elmpst  35578  istotbnd3  37817  sstotbnd2  37820  sstotbnd  37821  sstotbnd3  37822  equivtotbnd  37824  totbndbnd  37835  prdstotbnd  37840  isnacs3  42749  pwfi2f1o  43135  hbtlem6  43168