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

Theorem elfpw 7173
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 3371 . 2  |-  ( A  e.  ( ~P B  i^i  Fin )  <->  ( A  e.  ~P B  /\  A  e.  Fin ) )
2 elpwg 3645 . . 3  |-  ( A  e.  Fin  ->  ( A  e.  ~P B  <->  A 
C_  B ) )
32pm5.32ri 619 . 2  |-  ( ( A  e.  ~P B  /\  A  e.  Fin ) 
<->  ( A  C_  B  /\  A  e.  Fin ) )
41, 3bitri 240 1  |-  ( A  e.  ( ~P B  i^i  Fin )  <->  ( A  C_  B  /\  A  e. 
Fin ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 176    /\ wa 358    e. wcel 1696    i^i cin 3164    C_ wss 3165   ~Pcpw 3638   Fincfn 6879
This theorem is referenced by:  bitsinv2  12650  bitsf1ocnv  12651  2ebits  12654  bitsinvp1  12656  sadcaddlem  12664  sadadd2lem  12666  sadadd3  12668  sadaddlem  12673  sadasslem  12677  sadeq  12679  firest  13353  acsfiindd  14296  restfpw  16926  cmpcov2  17133  cmpcovf  17134  cncmp  17135  tgcmp  17144  cmpcld  17145  cmpfi  17151  alexsublem  17754  alexsubALTlem2  17758  alexsubALTlem4  17760  alexsubALT  17761  ptcmplem2  17763  ptcmplem3  17764  ptcmplem5  17766  tsmsfbas  17826  tsmslem1  17827  tsmsgsum  17837  tsmssubm  17841  tsmsres  17842  tsmsf1o  17843  tsmsmhm  17844  tsmsadd  17845  tsmsxplem1  17851  tsmsxplem2  17852  tsmsxp  17853  xrge0gsumle  18354  xrge0tsms  18355  xrge0tsmsd  23397  indf1ofs  23624  locfincmp  26407  comppfsc  26410  istotbnd3  26598  sstotbnd2  26601  sstotbnd  26602  sstotbnd3  26603  equivtotbnd  26605  totbndbnd  26616  prdstotbnd  26621  isnacs3  26888  pwfi2f1o  27363  hbtlem6  27436
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-v 2803  df-in 3172  df-ss 3179  df-pw 3640
  Copyright terms: Public domain W3C validator