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

Theorem elrabi 3254
Description: Implication for the membership in a restricted class abstraction. (Contributed by Alexander van der Vekens, 31-Dec-2017.)
Assertion
Ref Expression
elrabi
Distinct variable groups:   ,   ,

Proof of Theorem elrabi
StepHypRef Expression
1 clelab 2601 . . 3
2 eleq1 2529 . . . . . 6
32anbi1d 704 . . . . 5
43simprbda 623 . . . 4
54exlimiv 1722 . . 3
61, 5sylbi 195 . 2
7 df-rab 2816 . 2
86, 7eleq2s 2565 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369  =wceq 1395  E.wex 1612  e.wcel 1818  {cab 2442  {crab 2811
This theorem is referenced by:  elfvmptrab1  5976  elovmpt2rab  6521  elovmpt2rab1  6522  elovmpt3rab1  6536  mapfienlem1  7884  mapfienlem2  7885  mapfienlem3  7886  kmlem1  8551  fin1a2lem9  8809  nnind  10579  ublbneg  11195  supminf  11198  rlimrege0  13402  incexc2  13650  odcl  16560  odlem2  16563  gexcl  16600  gexlem2  16602  gexdvds  16604  pgpssslw  16634  resspsrmul  18072  mplbas2  18134  mptcoe1fsupp  18255  psropprmul  18279  coe1mul2  18310  psgnfix2  18635  psgndiflemB  18636  psgndif  18638  zrhcopsgndif  18639  cpmatpmat  19211  mptcoe1matfsupp  19303  mp2pm2mplem4  19310  chpscmat  19343  chpscmatgsumbin  19345  chpscmatgsummon  19346  txdis1cn  20136  ptcmplem3  20554  rrxmvallem  21831  mdegmullem  22478  0sgm  23418  sgmf  23419  sgmnncl  23421  dvdsdivcl  23457  fsumdvdsdiaglem  23459  fsumdvdscom  23461  dvdsppwf1o  23462  dvdsflf1o  23463  musumsum  23468  muinv  23469  sgmppw  23472  rpvmasumlem  23672  dchrmusum2  23679  dchrvmasumlem1  23680  dchrvmasum2lem  23681  dchrisum0fmul  23691  dchrisum0ff  23692  dchrisum0flblem1  23693  dchrisum0  23705  logsqvma  23727  usgraidx2v  24393  uvtxisvtx  24490  clwlkf1clwwlk  24850  2wlkonot3v  24875  2spthonot3v  24876  rusgranumwlks  24956  frgrawopreglem4  25047  frgrawopreg  25049  rabsnel  27402  nnindf  27610  ddemeas  28208  imambfm  28233  eulerpartlemgs2  28319  ballotlemfc0  28431  ballotlemfcc  28432  ballotlemirc  28470  mblfinlem2  30052  rencldnfilem  30754  irrapx1  30764  phisum  31159  radcnvrat  31195  lcmgcdlem  31212  dvnprodlem1  31743  stoweidlem15  31797  stoweidlem31  31813  fourierdlem25  31914  fourierdlem51  31940  fourierdlem79  31968  etransclem28  32045  usgresvm1  32443  usgresvm1ALT  32447  isinitoi  32609  istermoi  32610  2zrngasgrp  32746  2zrngamnd  32747  2zrngacmnd  32748  2zrngagrp  32749  2zrngmsgrp  32753  2zrngALT  32754  2zrngnmlid  32755  2zrngnmlid2  32757  bnj110  33916
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-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-rab 2816
  Copyright terms: Public domain W3C validator