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

Theorem elrabi 3092
Description: Implication for the membership in a restricted class abstraction. (Contributed by Alexander van der Vekens, 31-Dec-2017.)
Assertion
Ref Expression
elrabi  |-  ( A  e.  { x  e.  V  |  ph }  ->  A  e.  V )
Distinct variable groups:    x, A    x, V
Allowed substitution hint:    ph( x)

Proof of Theorem elrabi
StepHypRef Expression
1 clelab 2558 . . 3  |-  ( A  e.  { x  |  ( x  e.  V  /\  ph ) }  <->  E. x
( x  =  A  /\  ( x  e.  V  /\  ph )
) )
2 eleq1 2498 . . . . . 6  |-  ( x  =  A  ->  (
x  e.  V  <->  A  e.  V ) )
32anbi1d 687 . . . . 5  |-  ( x  =  A  ->  (
( x  e.  V  /\  ph )  <->  ( A  e.  V  /\  ph )
) )
43simprbda 608 . . . 4  |-  ( ( x  =  A  /\  ( x  e.  V  /\  ph ) )  ->  A  e.  V )
54exlimiv 1645 . . 3  |-  ( E. x ( x  =  A  /\  ( x  e.  V  /\  ph ) )  ->  A  e.  V )
61, 5sylbi 189 . 2  |-  ( A  e.  { x  |  ( x  e.  V  /\  ph ) }  ->  A  e.  V )
7 df-rab 2716 . 2  |-  { x  e.  V  |  ph }  =  { x  |  ( x  e.  V  /\  ph ) }
86, 7eleq2s 2530 1  |-  ( A  e.  { x  e.  V  |  ph }  ->  A  e.  V )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360   E.wex 1551    = wceq 1653    e. wcel 1726   {cab 2424   {crab 2711
This theorem is referenced by:  kmlem1  8032  fin1a2lem9  8290  nnind  10020  ublbneg  10562  supminf  10565  rlimrege0  12375  incexc2  12620  odcl  15176  odlem2  15179  gexcl  15216  gexlem2  15218  gexdvds  15220  pgpssslw  15250  resspsrmul  16482  psropprmul  16634  coe1mul2  16664  txdis1cn  17669  ptcmplem3  18087  mdegmullem  20003  0sgm  20929  sgmf  20930  sgmnncl  20932  dvdsdivcl  20968  fsumdvdsdiaglem  20970  fsumdvdscom  20972  dvdsppwf1o  20973  dvdsflf1o  20974  musumsum  20979  muinv  20980  sgmppw  20983  rpvmasumlem  21183  dchrmusum2  21190  dchrvmasumlem1  21191  dchrvmasum2lem  21192  dchrisum0fmul  21202  dchrisum0ff  21203  dchrisum0flblem1  21204  dchrisum0  21216  logsqvma  21238  usgraidx2v  21414  uvtxisvtx  21501  imambfm  24614  ballotlemfc0  24752  ballotlemfcc  24753  ballotlemirc  24791  mblfinlem2  26246  rencldnfilem  26883  irrapx1  26893  phisum  27497  stoweidlem15  27742  stoweidlem31  27758  elovmpt2rab  28092  elovmpt2rab1  28093  elovmpt3rab1  28095  2wlkonot3v  28395  2spthonot3v  28396  frgrawopreglem4  28498  frgrawopreg  28500  bnj110  29291
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-rab 2716
  Copyright terms: Public domain W3C validator