MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  elfpw Structured version   Visualization version   GIF version

Theorem elfpw 8812
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
StepHypRef Expression
1 elin 3934 . 2 (𝐴 ∈ (𝒫 𝐵 ∩ Fin) ↔ (𝐴 ∈ 𝒫 𝐵𝐴 ∈ Fin))
2 elpwg 4523 . . 3 (𝐴 ∈ Fin → (𝐴 ∈ 𝒫 𝐵𝐴𝐵))
32pm5.32ri 579 . 2 ((𝐴 ∈ 𝒫 𝐵𝐴 ∈ Fin) ↔ (𝐴𝐵𝐴 ∈ Fin))
41, 3bitri 278 1 (𝐴 ∈ (𝒫 𝐵 ∩ Fin) ↔ (𝐴𝐵𝐴 ∈ Fin))
Colors of variables: wff setvar class
Syntax hints:  wb 209  wa 399  wcel 2115  cin 3917  wss 3918  𝒫 cpw 4520  Fincfn 8494
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2964  df-v 3481  df-in 3925  df-ss 3935  df-pw 4522
This theorem is referenced by:  bitsinv2  15781  bitsf1ocnv  15782  2ebits  15785  bitsinvp1  15787  sadcaddlem  15795  sadadd2lem  15797  sadadd3  15799  sadaddlem  15804  sadasslem  15808  sadeq  15810  firest  16697  acsfiindd  17778  restfpw  21775  cmpcov2  21986  cmpcovf  21987  cncmp  21988  tgcmp  21997  cmpcld  21998  cmpfi  22004  locfincmp  22122  comppfsc  22128  alexsublem  22640  alexsubALTlem2  22644  alexsubALTlem4  22646  alexsubALT  22647  ptcmplem2  22649  ptcmplem3  22650  ptcmplem5  22652  tsmsfbas  22724  tsmslem1  22725  tsmsgsum  22735  tsmssubm  22739  tsmsres  22740  tsmsf1o  22741  tsmsmhm  22742  tsmsadd  22743  tsmsxplem1  22749  tsmsxplem2  22750  tsmsxp  22751  xrge0gsumle  23429  xrge0tsms  23430  xrge0tsmsd  30712  indf1ofs  31305  mvrsfpw  32773  elmpst  32803  istotbnd3  35114  sstotbnd2  35117  sstotbnd  35118  sstotbnd3  35119  equivtotbnd  35121  totbndbnd  35132  prdstotbnd  35137  isnacs3  39498  pwfi2f1o  39887  hbtlem6  39920
  Copyright terms: Public domain W3C validator