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

Theorem elfpw 7882
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  |-  ( A  e.  ( ~P B  i^i  Fin )  <->  ( A  C_  B  /\  A  e. 
Fin ) )

Proof of Theorem elfpw
StepHypRef Expression
1 elin 3655 . 2  |-  ( A  e.  ( ~P B  i^i  Fin )  <->  ( A  e.  ~P B  /\  A  e.  Fin ) )
2 elpwg 3993 . . 3  |-  ( A  e.  Fin  ->  ( A  e.  ~P B  <->  A 
C_  B ) )
32pm5.32ri 642 . 2  |-  ( ( A  e.  ~P B  /\  A  e.  Fin ) 
<->  ( A  C_  B  /\  A  e.  Fin ) )
41, 3bitri 252 1  |-  ( A  e.  ( ~P B  i^i  Fin )  <->  ( A  C_  B  /\  A  e. 
Fin ) )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 187    /\ wa 370    e. wcel 1870    i^i cin 3441    C_ wss 3442   ~Pcpw 3985   Fincfn 7577
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-v 3089  df-in 3449  df-ss 3456  df-pw 3987
This theorem is referenced by:  bitsinv2  14391  bitsf1ocnv  14392  2ebits  14395  bitsinvp1  14397  sadcaddlem  14405  sadadd2lem  14407  sadadd3  14409  sadaddlem  14414  sadasslem  14418  sadeq  14420  firest  15290  acsfiindd  16374  restfpw  20126  cmpcov2  20336  cmpcovf  20337  cncmp  20338  tgcmp  20347  cmpcld  20348  cmpfi  20354  locfincmp  20472  comppfsc  20478  alexsublem  20990  alexsubALTlem2  20994  alexsubALTlem4  20996  alexsubALT  20997  ptcmplem2  20999  ptcmplem3  21000  ptcmplem5  21002  tsmsfbas  21073  tsmslem1  21074  tsmsgsum  21084  tsmssubm  21088  tsmsres  21089  tsmsf1o  21090  tsmsmhm  21091  tsmsadd  21092  tsmsxplem1  21098  tsmsxplem2  21099  tsmsxp  21100  xrge0gsumle  21762  xrge0tsms  21763  xrge0tsmsd  28387  indf1ofs  28686  mvrsfpw  29932  elmpst  29962  istotbnd3  31807  sstotbnd2  31810  sstotbnd  31811  sstotbnd3  31812  equivtotbnd  31814  totbndbnd  31825  prdstotbnd  31830  isnacs3  35261  pwfi2f1o  35660  hbtlem6  35694
  Copyright terms: Public domain W3C validator