Theorem elfpw 7842

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

Proof of Theorem elfpw

Step	Hyp	Ref	Expression
1		elin 3686	. 2
2		elpwg 4020	. . 3
3	2	pm5.32ri 638	. 2
4	1, 3	bitri 249	1

Syntax hints:  <->wb 184  /\wa 369  e.wcel 1818  i^icin 3474  C_wss 3475  ~Pcpw 4012  cfn 7536

This theorem is referenced by:  bitsinv2  14093  bitsf1ocnv  14094  2ebits  14097  bitsinvp1  14099  sadcaddlem  14107  sadadd2lem  14109  sadadd3  14111  sadaddlem  14116  sadasslem  14120  sadeq  14122  firest  14830  acsfiindd  15807  restfpw  19680  cmpcov2  19890  cmpcovf  19891  cncmp  19892  tgcmp  19901  cmpcld  19902  cmpfi  19908  locfincmp  20027  comppfsc  20033  alexsublem  20544  alexsubALTlem2  20548  alexsubALTlem4  20550  alexsubALT  20551  ptcmplem2  20553  ptcmplem3  20554  ptcmplem5  20556  tsmsfbas  20626  tsmslem1  20627  tsmsgsum  20637  tsmsgsumOLD  20640  tsmssubm  20644  tsmsresOLD  20645  tsmsres  20646  tsmsf1o  20647  tsmsmhm  20648  tsmsadd  20649  tsmsxplem1  20655  tsmsxplem2  20656  tsmsxp  20657  xrge0gsumle  21338  xrge0tsms  21339  xrge0tsmsd  27775  indf1ofs  28039  mvrsfpw  28866  elmpst  28896  istotbnd3  30267  sstotbnd2  30270  sstotbnd  30271  sstotbnd3  30272  equivtotbnd  30274  totbndbnd  30285  prdstotbnd  30290  isnacs3  30642  pwfi2f1o  31044  hbtlem6  31078

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-v 3111  df-in 3482  df-ss 3489  df-pw 4014