Theorem elfpw 8212

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

Syntax hints:   ↔ wb 196   ∧ wa 384   ∈ wcel 1987   ∩ cin 3554   ⊆ wss 3555  𝒫 cpw 4130  Fincfn 7899

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-v 3188  df-in 3562  df-ss 3569  df-pw 4132

This theorem is referenced by:  bitsinv2  15089  bitsf1ocnv  15090  2ebits  15093  bitsinvp1  15095  sadcaddlem  15103  sadadd2lem  15105  sadadd3  15107  sadaddlem  15112  sadasslem  15116  sadeq  15118  firest  16014  acsfiindd  17098  restfpw  20893  cmpcov2  21103  cmpcovf  21104  cncmp  21105  tgcmp  21114  cmpcld  21115  cmpfi  21121  locfincmp  21239  comppfsc  21245  alexsublem  21758  alexsubALTlem2  21762  alexsubALTlem4  21764  alexsubALT  21765  ptcmplem2  21767  ptcmplem3  21768  ptcmplem5  21770  tsmsfbas  21841  tsmslem1  21842  tsmsgsum  21852  tsmssubm  21856  tsmsres  21857  tsmsf1o  21858  tsmsmhm  21859  tsmsadd  21860  tsmsxplem1  21866  tsmsxplem2  21867  tsmsxp  21868  xrge0gsumle  22544  xrge0tsms  22545  xrge0tsmsd  29567  indf1ofs  29866  mvrsfpw  31108  elmpst  31138  istotbnd3  33199  sstotbnd2  33202  sstotbnd  33203  sstotbnd3  33204  equivtotbnd  33206  totbndbnd  33217  prdstotbnd  33222  isnacs3  36750  pwfi2f1o  37143  hbtlem6  37177