Theorem elfpw 9354

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

Syntax hints:   ↔ wb 205   ∧ wa 397   ∈ wcel 2107   ∩ cin 3948   ⊆ wss 3949  𝒫 cpw 4603  Fincfn 8939

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-in 3956  df-ss 3966  df-pw 4605

This theorem is referenced by:  bitsinv2  16384  bitsf1ocnv  16385  2ebits  16388  bitsinvp1  16390  sadcaddlem  16398  sadadd2lem  16400  sadadd3  16402  sadaddlem  16407  sadasslem  16411  sadeq  16413  firest  17378  acsfiindd  18506  restfpw  22683  cmpcov2  22894  cmpcovf  22895  cncmp  22896  tgcmp  22905  cmpcld  22906  cmpfi  22912  locfincmp  23030  comppfsc  23036  alexsublem  23548  alexsubALTlem2  23552  alexsubALTlem4  23554  alexsubALT  23555  ptcmplem2  23557  ptcmplem3  23558  ptcmplem5  23560  tsmsfbas  23632  tsmslem1  23633  tsmsgsum  23643  tsmssubm  23647  tsmsres  23648  tsmsf1o  23649  tsmsmhm  23650  tsmsadd  23651  tsmsxplem1  23657  tsmsxplem2  23658  tsmsxp  23659  xrge0gsumle  24349  xrge0tsms  24350  xrge0tsmsd  32209  indf1ofs  33024  mvrsfpw  34497  elmpst  34527  istotbnd3  36639  sstotbnd2  36642  sstotbnd  36643  sstotbnd3  36644  equivtotbnd  36646  totbndbnd  36657  prdstotbnd  36662  isnacs3  41448  pwfi2f1o  41838  hbtlem6  41871