Theorem elfpw 9321

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 3924	. 2 ⊢ (𝐴 ∈ (𝒫 𝐵 ∩ Fin) ↔ (𝐴 ∈ 𝒫 𝐵 ∧ 𝐴 ∈ Fin))
2		elpwg 4570	. . 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 2146   ∩ cin 3907   ⊆ wss 3908  𝒫 cpw 4567  Fincfn 8952

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 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-v 3460  df-in 3915  df-ss 3925  df-pw 4569

This theorem is used by:  bitsinv2  16526  bitsf1ocnv  16527  2ebits  16530  bitsinvp1  16532  sadcaddlem  16540  sadadd2lem  16542  sadadd3  16544  sadaddlem  16549  sadasslem  16553  sadeq  16555  firest  17510  acsfiindd  18634  restfpw  23373  cmpcov2  23584  cmpcovf  23585  cncmp  23586  tgcmp  23595  cmpcld  23596  cmpfi  23602  locfincmp  23720  comppfsc  23726  alexsublem  24238  alexsubALTlem2  24242  alexsubALTlem4  24244  alexsubALT  24245  ptcmplem2  24247  ptcmplem3  24248  ptcmplem5  24250  tsmsfbas  24322  tsmslem1  24323  tsmsgsum  24333  tsmssubm  24337  tsmsres  24338  tsmsf1o  24339  tsmsmhm  24340  tsmsadd  24341  tsmsxplem1  24347  tsmsxplem2  24348  tsmsxp  24349  xrge0gsumle  25028  xrge0tsms  25029  indf1ofs  33223  xrge0tsmsd  33424  mvrsfpw  36019  elmpst  36049  istotbnd3  38463  sstotbnd2  38466  sstotbnd  38467  sstotbnd3  38468  equivtotbnd  38470  totbndbnd  38481  prdstotbnd  38486  isnacs3  43482  pwfi2f1o  43864  hbtlem6  43897