Theorem elfpw 9343

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 3915	. 2 ⊢ (𝐴 ∈ (𝒫 𝐵 ∩ Fin) ↔ (𝐴 ∈ 𝒫 𝐵 ∧ 𝐴 ∈ Fin))
2		elpwg 4560	. . 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 2145   ∩ cin 3898   ⊆ wss 3899  𝒫 cpw 4557  Fincfn 8973

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 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-in 3906  df-ss 3916  df-pw 4559

This theorem is used by:  bitsinv2  16613  bitsf1ocnv  16614  2ebits  16617  bitsinvp1  16619  sadcaddlem  16627  sadadd2lem  16629  sadadd3  16631  sadaddlem  16636  sadasslem  16640  sadeq  16642  firest  17603  acsfiindd  18727  restfpw  23497  cmpcov2  23708  cmpcovf  23709  cncmp  23710  tgcmp  23719  cmpcld  23720  cmpfi  23726  locfincmp  23845  comppfsc  23851  alexsublem  24363  alexsubALTlem2  24367  alexsubALTlem4  24369  alexsubALT  24370  ptcmplem2  24372  ptcmplem3  24373  ptcmplem5  24375  tsmsfbas  24447  tsmslem1  24448  tsmsgsum  24458  tsmssubm  24462  tsmsres  24463  tsmsf1o  24464  tsmsmhm  24465  tsmsadd  24466  tsmsxplem1  24472  tsmsxplem2  24473  tsmsxp  24474  xrge0gsumle  25153  xrge0tsms  25154  indf1ofs  33433  xrge0tsmsd  33634  mvrsfpw  36271  elmpst  36301  istotbnd3  38705  sstotbnd2  38708  sstotbnd  38709  sstotbnd3  38710  equivtotbnd  38712  totbndbnd  38723  prdstotbnd  38728  isnacs3  43720  pwfi2f1o  44097  hbtlem6  44130