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

Theorem elfpw 7400
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 3522 . 2  |-  ( A  e.  ( ~P B  i^i  Fin )  <->  ( A  e.  ~P B  /\  A  e.  Fin ) )
2 elpwg 3798 . . 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 1725    i^i cin 3311    C_ wss 3312   ~Pcpw 3791   Fincfn 7101
This theorem is referenced by:  bitsinv2  12947  bitsf1ocnv  12948  2ebits  12951  bitsinvp1  12953  sadcaddlem  12961  sadadd2lem  12963  sadadd3  12965  sadaddlem  12970  sadasslem  12974  sadeq  12976  firest  13652  acsfiindd  14595  restfpw  17235  cmpcov2  17445  cmpcovf  17446  cncmp  17447  tgcmp  17456  cmpcld  17457  cmpfi  17463  alexsublem  18067  alexsubALTlem2  18071  alexsubALTlem4  18073  alexsubALT  18074  ptcmplem2  18076  ptcmplem3  18077  ptcmplem5  18079  tsmsfbas  18149  tsmslem1  18150  tsmsgsum  18160  tsmssubm  18164  tsmsres  18165  tsmsf1o  18166  tsmsmhm  18167  tsmsadd  18168  tsmsxplem1  18174  tsmsxplem2  18175  tsmsxp  18176  xrge0gsumle  18856  xrge0tsms  18857  xrge0tsmsd  24215  indf1ofs  24415  locfincmp  26375  comppfsc  26378  istotbnd3  26471  sstotbnd2  26474  sstotbnd  26475  sstotbnd3  26476  equivtotbnd  26478  totbndbnd  26489  prdstotbnd  26494  isnacs3  26755  pwfi2f1o  27228  hbtlem6  27301
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-v 2950  df-in 3319  df-ss 3326  df-pw 3793
  Copyright terms: Public domain W3C validator