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

Theorem elfpw 7822
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 3687 . 2  |-  ( A  e.  ( ~P B  i^i  Fin )  <->  ( A  e.  ~P B  /\  A  e.  Fin ) )
2 elpwg 4018 . . 3  |-  ( A  e.  Fin  ->  ( A  e.  ~P B  <->  A 
C_  B ) )
32pm5.32ri 638 . 2  |-  ( ( A  e.  ~P B  /\  A  e.  Fin ) 
<->  ( A  C_  B  /\  A  e.  Fin ) )
41, 3bitri 249 1  |-  ( A  e.  ( ~P B  i^i  Fin )  <->  ( A  C_  B  /\  A  e. 
Fin ) )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    /\ wa 369    e. wcel 1767    i^i cin 3475    C_ wss 3476   ~Pcpw 4010   Fincfn 7516
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-v 3115  df-in 3483  df-ss 3490  df-pw 4012
This theorem is referenced by:  bitsinv2  13952  bitsf1ocnv  13953  2ebits  13956  bitsinvp1  13958  sadcaddlem  13966  sadadd2lem  13968  sadadd3  13970  sadaddlem  13975  sadasslem  13979  sadeq  13981  firest  14688  acsfiindd  15664  restfpw  19474  cmpcov2  19684  cmpcovf  19685  cncmp  19686  tgcmp  19695  cmpcld  19696  cmpfi  19702  alexsublem  20307  alexsubALTlem2  20311  alexsubALTlem4  20313  alexsubALT  20314  ptcmplem2  20316  ptcmplem3  20317  ptcmplem5  20319  tsmsfbas  20389  tsmslem1  20390  tsmsgsum  20400  tsmsgsumOLD  20403  tsmssubm  20407  tsmsresOLD  20408  tsmsres  20409  tsmsf1o  20410  tsmsmhm  20411  tsmsadd  20412  tsmsxplem1  20418  tsmsxplem2  20419  tsmsxp  20420  xrge0gsumle  21101  xrge0tsms  21102  xrge0tsmsd  27466  indf1ofs  27707  locfincmp  29804  comppfsc  29807  istotbnd3  29898  sstotbnd2  29901  sstotbnd  29902  sstotbnd3  29903  equivtotbnd  29905  totbndbnd  29916  prdstotbnd  29921  isnacs3  30274  pwfi2f1o  30676  hbtlem6  30710
  Copyright terms: Public domain W3C validator