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

Theorem elfpw 7601
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 3527 . 2  |-  ( A  e.  ( ~P B  i^i  Fin )  <->  ( A  e.  ~P B  /\  A  e.  Fin ) )
2 elpwg 3856 . . 3  |-  ( A  e.  Fin  ->  ( A  e.  ~P B  <->  A 
C_  B ) )
32pm5.32ri 631 . 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 1755    i^i cin 3315    C_ wss 3316   ~Pcpw 3848   Fincfn 7298
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-v 2964  df-in 3323  df-ss 3330  df-pw 3850
This theorem is referenced by:  bitsinv2  13621  bitsf1ocnv  13622  2ebits  13625  bitsinvp1  13627  sadcaddlem  13635  sadadd2lem  13637  sadadd3  13639  sadaddlem  13644  sadasslem  13648  sadeq  13650  firest  14353  acsfiindd  15329  restfpw  18624  cmpcov2  18834  cmpcovf  18835  cncmp  18836  tgcmp  18845  cmpcld  18846  cmpfi  18852  alexsublem  19457  alexsubALTlem2  19461  alexsubALTlem4  19463  alexsubALT  19464  ptcmplem2  19466  ptcmplem3  19467  ptcmplem5  19469  tsmsfbas  19539  tsmslem1  19540  tsmsgsum  19550  tsmsgsumOLD  19553  tsmssubm  19557  tsmsresOLD  19558  tsmsres  19559  tsmsf1o  19560  tsmsmhm  19561  tsmsadd  19562  tsmsxplem1  19568  tsmsxplem2  19569  tsmsxp  19570  xrge0gsumle  20251  xrge0tsms  20252  xrge0tsmsd  26105  indf1ofs  26335  locfincmp  28417  comppfsc  28420  istotbnd3  28511  sstotbnd2  28514  sstotbnd  28515  sstotbnd3  28516  equivtotbnd  28518  totbndbnd  28529  prdstotbnd  28534  isnacs3  28888  pwfi2f1o  29293  hbtlem6  29327
  Copyright terms: Public domain W3C validator