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

Theorem elfpw 7886
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 3649 . 2  |-  ( A  e.  ( ~P B  i^i  Fin )  <->  ( A  e.  ~P B  /\  A  e.  Fin ) )
2 elpwg 3989 . . 3  |-  ( A  e.  Fin  ->  ( A  e.  ~P B  <->  A 
C_  B ) )
32pm5.32ri 642 . 2  |-  ( ( A  e.  ~P B  /\  A  e.  Fin ) 
<->  ( A  C_  B  /\  A  e.  Fin ) )
41, 3bitri 252 1  |-  ( A  e.  ( ~P B  i^i  Fin )  <->  ( A  C_  B  /\  A  e. 
Fin ) )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 187    /\ wa 370    e. wcel 1872    i^i cin 3435    C_ wss 3436   ~Pcpw 3981   Fincfn 7581
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2568  df-v 3082  df-in 3443  df-ss 3450  df-pw 3983
This theorem is referenced by:  bitsinv2  14417  bitsf1ocnv  14418  2ebits  14421  bitsinvp1  14423  sadcaddlem  14431  sadadd2lem  14433  sadadd3  14435  sadaddlem  14440  sadasslem  14444  sadeq  14446  firest  15331  acsfiindd  16423  restfpw  20194  cmpcov2  20404  cmpcovf  20405  cncmp  20406  tgcmp  20415  cmpcld  20416  cmpfi  20422  locfincmp  20540  comppfsc  20546  alexsublem  21058  alexsubALTlem2  21062  alexsubALTlem4  21064  alexsubALT  21065  ptcmplem2  21067  ptcmplem3  21068  ptcmplem5  21070  tsmsfbas  21141  tsmslem1  21142  tsmsgsum  21152  tsmssubm  21156  tsmsres  21157  tsmsf1o  21158  tsmsmhm  21159  tsmsadd  21160  tsmsxplem1  21166  tsmsxplem2  21167  tsmsxp  21168  xrge0gsumle  21850  xrge0tsms  21851  xrge0tsmsd  28557  indf1ofs  28856  mvrsfpw  30153  elmpst  30183  istotbnd3  32068  sstotbnd2  32071  sstotbnd  32072  sstotbnd3  32073  equivtotbnd  32075  totbndbnd  32086  prdstotbnd  32091  isnacs3  35522  pwfi2f1o  35925  hbtlem6  35959
  Copyright terms: Public domain W3C validator