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

Theorem elfpw 7157
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 3358 . 2  |-  ( A  e.  ( ~P B  i^i  Fin )  <->  ( A  e.  ~P B  /\  A  e.  Fin ) )
2 elpwg 3632 . . 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 1684    i^i cin 3151    C_ wss 3152   ~Pcpw 3625   Fincfn 6863
This theorem is referenced by:  bitsinv2  12634  bitsf1ocnv  12635  2ebits  12638  bitsinvp1  12640  sadcaddlem  12648  sadadd2lem  12650  sadadd3  12652  sadaddlem  12657  sadasslem  12661  sadeq  12663  firest  13337  acsfiindd  14280  restfpw  16910  cmpcov2  17117  cmpcovf  17118  cncmp  17119  tgcmp  17128  cmpcld  17129  cmpfi  17135  alexsublem  17738  alexsubALTlem2  17742  alexsubALTlem4  17744  alexsubALT  17745  ptcmplem2  17747  ptcmplem3  17748  ptcmplem5  17750  tsmsfbas  17810  tsmslem1  17811  tsmsgsum  17821  tsmssubm  17825  tsmsres  17826  tsmsf1o  17827  tsmsmhm  17828  tsmsadd  17829  tsmsxplem1  17835  tsmsxplem2  17836  tsmsxp  17837  xrge0gsumle  18338  xrge0tsms  18339  xrge0tsmsd  23382  indf1ofs  23609  locfincmp  26304  comppfsc  26307  istotbnd3  26495  sstotbnd2  26498  sstotbnd  26499  sstotbnd3  26500  equivtotbnd  26502  totbndbnd  26513  prdstotbnd  26518  isnacs3  26785  pwfi2f1o  27260  hbtlem6  27333
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-v 2790  df-in 3159  df-ss 3166  df-pw 3627
  Copyright terms: Public domain W3C validator