Theorem elfpw 9261

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 3906	. 2 ⊢ (𝐴 ∈ (𝒫 𝐵 ∩ Fin) ↔ (𝐴 ∈ 𝒫 𝐵 ∧ 𝐴 ∈ Fin))
2		elpwg 4539	. . 3 ⊢ (𝐴 ∈ Fin → (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵))
3	2	pm5.32ri 580	. 2 ⊢ ((𝐴 ∈ 𝒫 𝐵 ∧ 𝐴 ∈ Fin) ↔ (𝐴 ⊆ 𝐵 ∧ 𝐴 ∈ Fin))
4	1, 3	bitri 276	1 ⊢ (𝐴 ∈ (𝒫 𝐵 ∩ Fin) ↔ (𝐴 ⊆ 𝐵 ∧ 𝐴 ∈ Fin))

Syntax hints:   ↔ wb 207   ∧ wa 396   ∈ wcel 2119   ∩ cin 3889   ⊆ wss 3890  𝒫 cpw 4536  Fincfn 8890

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-v 3434  df-in 3897  df-ss 3907  df-pw 4538

This theorem is referenced by:  bitsinv2  16410  bitsf1ocnv  16411  2ebits  16414  bitsinvp1  16416  sadcaddlem  16424  sadadd2lem  16426  sadadd3  16428  sadaddlem  16433  sadasslem  16437  sadeq  16439  firest  17393  acsfiindd  18517  restfpw  23169  cmpcov2  23380  cmpcovf  23381  cncmp  23382  tgcmp  23391  cmpcld  23392  cmpfi  23398  locfincmp  23516  comppfsc  23522  alexsublem  24034  alexsubALTlem2  24038  alexsubALTlem4  24040  alexsubALT  24041  ptcmplem2  24043  ptcmplem3  24044  ptcmplem5  24046  tsmsfbas  24118  tsmslem1  24119  tsmsgsum  24129  tsmssubm  24133  tsmsres  24134  tsmsf1o  24135  tsmsmhm  24136  tsmsadd  24137  tsmsxplem1  24143  tsmsxplem2  24144  tsmsxp  24145  xrge0gsumle  24824  xrge0tsms  24825  indf1ofs  32952  xrge0tsmsd  33161  mvrsfpw  35741  elmpst  35771  istotbnd3  38145  sstotbnd2  38148  sstotbnd  38149  sstotbnd3  38150  equivtotbnd  38152  totbndbnd  38163  prdstotbnd  38168  isnacs3  43166  pwfi2f1o  43548  hbtlem6  43581