Theorem elrabi 3258

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

Step	Hyp	Ref	Expression
1		clelab 2611	. . 3 |- ( A e. { x | ( x e. V /\ ph ) } <-> E. x ( x = A /\ ( x e. V /\ ph ) ) )
2		eleq1 2539	. . . . . 6 |- ( x = A -> ( x e. V <-> A e. V ) )
3	2	anbi1d 704	. . . . 5 |- ( x = A -> ( ( x e. V /\ ph ) <-> ( A e. V /\ ph ) ) )
4	3	simprbda 623	. . . 4 |- ( ( x = A /\ ( x e. V /\ ph ) ) -> A e. V )
5	4	exlimiv 1698	. . 3 |- ( E. x ( x = A /\ ( x e. V /\ ph ) ) -> A e. V )
6	1, 5	sylbi 195	. 2 |- ( A e. { x | ( x e. V /\ ph ) } -> A e. V )
7		df-rab 2823	. 2 |- { x e. V | ph } = { x | ( x e. V /\ ph ) }
8	6, 7	eleq2s 2575	1 |- ( A e. { x e. V | ph } -> A e. V )

Syntax hints:   -> wi 4   /\ wa 369   = wceq 1379   E.wex 1596   e. wcel 1767   {cab 2452   {crab 2818

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-rab 2823

This theorem is referenced by:  elfvmptrab1  5970  elovmpt2rab  6505  elovmpt2rab1  6506  elovmpt3rab1  6520  mapfienlem1  7864  mapfienlem2  7865  mapfienlem3  7866  kmlem1  8530  fin1a2lem9  8788  nnind  10554  ublbneg  11166  supminf  11169  rlimrege0  13365  incexc2  13613  odcl  16366  odlem2  16369  gexcl  16406  gexlem2  16408  gexdvds  16410  pgpssslw  16440  resspsrmul  17871  mplbas2  17933  mptcoe1fsupp  18054  psropprmul  18078  coe1mul2  18109  psgnfix2  18430  psgndiflemB  18431  psgndif  18433  zrhcopsgndif  18434  cpmatpmat  19006  mptcoe1matfsupp  19098  mp2pm2mplem4  19105  chpscmat  19138  chpscmatgsumbin  19140  chpscmatgsummon  19141  txdis1cn  19899  ptcmplem3  20317  rrxmvallem  21594  mdegmullem  22241  0sgm  23174  sgmf  23175  sgmnncl  23177  dvdsdivcl  23213  fsumdvdsdiaglem  23215  fsumdvdscom  23217  dvdsppwf1o  23218  dvdsflf1o  23219  musumsum  23224  muinv  23225  sgmppw  23228  rpvmasumlem  23428  dchrmusum2  23435  dchrvmasumlem1  23436  dchrvmasum2lem  23437  dchrisum0fmul  23447  dchrisum0ff  23448  dchrisum0flblem1  23449  dchrisum0  23461  logsqvma  23483  usgraidx2v  24097  uvtxisvtx  24194  clwlkf1clwwlk  24554  2wlkonot3v  24579  2spthonot3v  24580  frgrawopreglem4  24752  frgrawopreg  24754  rabsnel  27106  nnindf  27306  ddemeas  27876  imambfm  27901  eulerpartlemgs2  27987  ballotlemfc0  28099  ballotlemfcc  28100  ballotlemirc  28138  mblfinlem2  29657  rencldnfilem  30386  irrapx1  30396  phisum  30792  lcmgcdlem  30840  stoweidlem15  31343  stoweidlem31  31359  usgresvm1  31938  usgresvm1ALT  31942  bnj110  33013