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

Theorem elfpw 7634
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 3560 . 2  |-  ( A  e.  ( ~P B  i^i  Fin )  <->  ( A  e.  ~P B  /\  A  e.  Fin ) )
2 elpwg 3889 . . 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 1756    i^i cin 3348    C_ wss 3349   ~Pcpw 3881   Fincfn 7331
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-v 2995  df-in 3356  df-ss 3363  df-pw 3883
This theorem is referenced by:  bitsinv2  13660  bitsf1ocnv  13661  2ebits  13664  bitsinvp1  13666  sadcaddlem  13674  sadadd2lem  13676  sadadd3  13678  sadaddlem  13683  sadasslem  13687  sadeq  13689  firest  14392  acsfiindd  15368  restfpw  18805  cmpcov2  19015  cmpcovf  19016  cncmp  19017  tgcmp  19026  cmpcld  19027  cmpfi  19033  alexsublem  19638  alexsubALTlem2  19642  alexsubALTlem4  19644  alexsubALT  19645  ptcmplem2  19647  ptcmplem3  19648  ptcmplem5  19650  tsmsfbas  19720  tsmslem1  19721  tsmsgsum  19731  tsmsgsumOLD  19734  tsmssubm  19738  tsmsresOLD  19739  tsmsres  19740  tsmsf1o  19741  tsmsmhm  19742  tsmsadd  19743  tsmsxplem1  19749  tsmsxplem2  19750  tsmsxp  19751  xrge0gsumle  20432  xrge0tsms  20433  xrge0tsmsd  26275  indf1ofs  26504  locfincmp  28602  comppfsc  28605  istotbnd3  28696  sstotbnd2  28699  sstotbnd  28700  sstotbnd3  28701  equivtotbnd  28703  totbndbnd  28714  prdstotbnd  28719  isnacs3  29072  pwfi2f1o  29477  hbtlem6  29511
  Copyright terms: Public domain W3C validator