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

Theorem elfpw 7366
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 3490 . 2  |-  ( A  e.  ( ~P B  i^i  Fin )  <->  ( A  e.  ~P B  /\  A  e.  Fin ) )
2 elpwg 3766 . . 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 1721    i^i cin 3279    C_ wss 3280   ~Pcpw 3759   Fincfn 7068
This theorem is referenced by:  bitsinv2  12910  bitsf1ocnv  12911  2ebits  12914  bitsinvp1  12916  sadcaddlem  12924  sadadd2lem  12926  sadadd3  12928  sadaddlem  12933  sadasslem  12937  sadeq  12939  firest  13615  acsfiindd  14558  restfpw  17197  cmpcov2  17407  cmpcovf  17408  cncmp  17409  tgcmp  17418  cmpcld  17419  cmpfi  17425  alexsublem  18028  alexsubALTlem2  18032  alexsubALTlem4  18034  alexsubALT  18035  ptcmplem2  18037  ptcmplem3  18038  ptcmplem5  18040  tsmsfbas  18110  tsmslem1  18111  tsmsgsum  18121  tsmssubm  18125  tsmsres  18126  tsmsf1o  18127  tsmsmhm  18128  tsmsadd  18129  tsmsxplem1  18135  tsmsxplem2  18136  tsmsxp  18137  xrge0gsumle  18817  xrge0tsms  18818  xrge0tsmsd  24176  indf1ofs  24376  locfincmp  26274  comppfsc  26277  istotbnd3  26370  sstotbnd2  26373  sstotbnd  26374  sstotbnd3  26375  equivtotbnd  26377  totbndbnd  26388  prdstotbnd  26393  isnacs3  26654  pwfi2f1o  27128  hbtlem6  27201
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 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-v 2918  df-in 3287  df-ss 3294  df-pw 3761
  Copyright terms: Public domain W3C validator