Theorem elfpw 9327

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 8957

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  16593  bitsf1ocnv  16594  2ebits  16597  bitsinvp1  16599  sadcaddlem  16607  sadadd2lem  16609  sadadd3  16611  sadaddlem  16616  sadasslem  16620  sadeq  16622  firest  17583  acsfiindd  18707  restfpw  23477  cmpcov2  23688  cmpcovf  23689  cncmp  23690  tgcmp  23699  cmpcld  23700  cmpfi  23706  locfincmp  23825  comppfsc  23831  alexsublem  24343  alexsubALTlem2  24347  alexsubALTlem4  24349  alexsubALT  24350  ptcmplem2  24352  ptcmplem3  24353  ptcmplem5  24355  tsmsfbas  24427  tsmslem1  24428  tsmsgsum  24438  tsmssubm  24442  tsmsres  24443  tsmsf1o  24444  tsmsmhm  24445  tsmsadd  24446  tsmsxplem1  24452  tsmsxplem2  24453  tsmsxp  24454  xrge0gsumle  25133  xrge0tsms  25134  indf1ofs  33415  xrge0tsmsd  33616  mvrsfpw  36240  elmpst  36270  istotbnd3  38673  sstotbnd2  38676  sstotbnd  38677  sstotbnd3  38678  equivtotbnd  38680  totbndbnd  38691  prdstotbnd  38696  isnacs3  43674  pwfi2f1o  44056  hbtlem6  44089