Theorem elfpw 8268

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

Syntax hints:   ↔ wb 196   ∧ wa 384   ∈ wcel 1990   ∩ cin 3573   ⊆ wss 3574  𝒫 cpw 4158  Fincfn 7955

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-in 3581  df-ss 3588  df-pw 4160

This theorem is referenced by:  bitsinv2  15165  bitsf1ocnv  15166  2ebits  15169  bitsinvp1  15171  sadcaddlem  15179  sadadd2lem  15181  sadadd3  15183  sadaddlem  15188  sadasslem  15192  sadeq  15194  firest  16093  acsfiindd  17177  restfpw  20983  cmpcov2  21193  cmpcovf  21194  cncmp  21195  tgcmp  21204  cmpcld  21205  cmpfi  21211  locfincmp  21329  comppfsc  21335  alexsublem  21848  alexsubALTlem2  21852  alexsubALTlem4  21854  alexsubALT  21855  ptcmplem2  21857  ptcmplem3  21858  ptcmplem5  21860  tsmsfbas  21931  tsmslem1  21932  tsmsgsum  21942  tsmssubm  21946  tsmsres  21947  tsmsf1o  21948  tsmsmhm  21949  tsmsadd  21950  tsmsxplem1  21956  tsmsxplem2  21957  tsmsxp  21958  xrge0gsumle  22636  xrge0tsms  22637  xrge0tsmsd  29785  indf1ofs  30088  mvrsfpw  31403  elmpst  31433  istotbnd3  33570  sstotbnd2  33573  sstotbnd  33574  sstotbnd3  33575  equivtotbnd  33577  totbndbnd  33588  prdstotbnd  33593  isnacs3  37273  pwfi2f1o  37666  hbtlem6  37699