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

Theorem elfpw 7345
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 3475 . 2  |-  ( A  e.  ( ~P B  i^i  Fin )  <->  ( A  e.  ~P B  /\  A  e.  Fin ) )
2 elpwg 3751 . . 3  |-  ( A  e.  Fin  ->  ( A  e.  ~P B  <->  A 
C_  B ) )
32pm5.32ri 620 . 2  |-  ( ( A  e.  ~P B  /\  A  e.  Fin ) 
<->  ( A  C_  B  /\  A  e.  Fin ) )
41, 3bitri 241 1  |-  ( A  e.  ( ~P B  i^i  Fin )  <->  ( A  C_  B  /\  A  e. 
Fin ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 177    /\ wa 359    e. wcel 1717    i^i cin 3264    C_ wss 3265   ~Pcpw 3744   Fincfn 7047
This theorem is referenced by:  bitsinv2  12884  bitsf1ocnv  12885  2ebits  12888  bitsinvp1  12890  sadcaddlem  12898  sadadd2lem  12900  sadadd3  12902  sadaddlem  12907  sadasslem  12911  sadeq  12913  firest  13589  acsfiindd  14532  restfpw  17167  cmpcov2  17377  cmpcovf  17378  cncmp  17379  tgcmp  17388  cmpcld  17389  cmpfi  17395  alexsublem  17998  alexsubALTlem2  18002  alexsubALTlem4  18004  alexsubALT  18005  ptcmplem2  18007  ptcmplem3  18008  ptcmplem5  18010  tsmsfbas  18080  tsmslem1  18081  tsmsgsum  18091  tsmssubm  18095  tsmsres  18096  tsmsf1o  18097  tsmsmhm  18098  tsmsadd  18099  tsmsxplem1  18105  tsmsxplem2  18106  tsmsxp  18107  xrge0gsumle  18737  xrge0tsms  18738  xrge0tsmsd  24054  indf1ofs  24221  locfincmp  26077  comppfsc  26080  istotbnd3  26173  sstotbnd2  26176  sstotbnd  26177  sstotbnd3  26178  equivtotbnd  26180  totbndbnd  26191  prdstotbnd  26196  isnacs3  26457  pwfi2f1o  26931  hbtlem6  27004
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2370
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2376  df-cleq 2382  df-clel 2385  df-nfc 2514  df-v 2903  df-in 3272  df-ss 3279  df-pw 3746
  Copyright terms: Public domain W3C validator