Theorem elfpw 8435

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

Syntax hints:   ↔ wb 196   ∧ wa 383   ∈ wcel 2139   ∩ cin 3714   ⊆ wss 3715  𝒫 cpw 4302  Fincfn 8123

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-v 3342  df-in 3722  df-ss 3729  df-pw 4304

This theorem is referenced by:  bitsinv2  15387  bitsf1ocnv  15388  2ebits  15391  bitsinvp1  15393  sadcaddlem  15401  sadadd2lem  15403  sadadd3  15405  sadaddlem  15410  sadasslem  15414  sadeq  15416  firest  16315  acsfiindd  17398  restfpw  21205  cmpcov2  21415  cmpcovf  21416  cncmp  21417  tgcmp  21426  cmpcld  21427  cmpfi  21433  locfincmp  21551  comppfsc  21557  alexsublem  22069  alexsubALTlem2  22073  alexsubALTlem4  22075  alexsubALT  22076  ptcmplem2  22078  ptcmplem3  22079  ptcmplem5  22081  tsmsfbas  22152  tsmslem1  22153  tsmsgsum  22163  tsmssubm  22167  tsmsres  22168  tsmsf1o  22169  tsmsmhm  22170  tsmsadd  22171  tsmsxplem1  22177  tsmsxplem2  22178  tsmsxp  22179  xrge0gsumle  22857  xrge0tsms  22858  xrge0tsmsd  30115  indf1ofs  30418  mvrsfpw  31731  elmpst  31761  istotbnd3  33901  sstotbnd2  33904  sstotbnd  33905  sstotbnd3  33906  equivtotbnd  33908  totbndbnd  33919  prdstotbnd  33924  isnacs3  37793  pwfi2f1o  38186  hbtlem6  38219