Theorem elfpw 9346

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 4093	. 2 ⊢ (𝐴 ∈ (𝒫 𝐵 ∩ Fin) ↔ (𝐴 ∈ 𝒫 𝐵 ∧ 𝐴 ∈ Fin))
2		elpwg 4559	. . 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 2144   ⊆ wss 3895   ∩ cin 4089  𝒫 cpw 4556  Fincfn 8976

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-ss 3896  df-in 4091  df-pw 4558

This theorem is used by:  bitsinv2  16618  bitsf1ocnv  16619  2ebits  16622  bitsinvp1  16624  sadcaddlem  16632  sadadd2lem  16634  sadadd3  16636  sadaddlem  16641  sadasslem  16645  sadeq  16647  firest  17608  acsfiindd  18732  restfpw  23502  cmpcov2  23713  cmpcovf  23714  cncmp  23715  tgcmp  23724  cmpcld  23725  cmpfi  23731  locfincmp  23850  comppfsc  23856  alexsublem  24368  alexsubALTlem2  24372  alexsubALTlem4  24374  alexsubALT  24375  ptcmplem2  24377  ptcmplem3  24378  ptcmplem5  24380  tsmsfbas  24452  tsmslem1  24453  tsmsgsum  24463  tsmssubm  24467  tsmsres  24468  tsmsf1o  24469  tsmsmhm  24470  tsmsadd  24471  tsmsxplem1  24477  tsmsxplem2  24478  tsmsxp  24479  xrge0gsumle  25158  xrge0tsms  25159  indf1ofs  33479  xrge0tsmsd  33680  mvrsfpw  36357  elmpst  36387  istotbnd3  38798  sstotbnd2  38801  sstotbnd  38802  sstotbnd3  38803  equivtotbnd  38805  totbndbnd  38816  prdstotbnd  38821  isnacs3  43814  pwfi2f1o  44191  hbtlem6  44224