Theorem elrabi 3103

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 2553	. . 3 |- ( A e. { x | ( x e. V /\ ph ) } <-> E. x ( x = A /\ ( x e. V /\ ph ) ) )
2		eleq1 2493	. . . . . 6 |- ( x = A -> ( x e. V <-> A e. V ) )
3	2	anbi1d 697	. . . . 5 |- ( x = A -> ( ( x e. V /\ ph ) <-> ( A e. V /\ ph ) ) )
4	3	simprbda 618	. . . 4 |- ( ( x = A /\ ( x e. V /\ ph ) ) -> A e. V )
5	4	exlimiv 1687	. . 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 2714	. 2 |- { x e. V | ph } = { x | ( x e. V /\ ph ) }
8	6, 7	eleq2s 2525	1 |- ( A e. { x e. V | ph } -> A e. V )

Syntax hints:   -> wi 4   /\ wa 369   = wceq 1362   E.wex 1589   e. wcel 1755   {cab 2419   {crab 2709

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-rab 2714

This theorem is referenced by:  mapfienlem1  7642  mapfienlem2  7643  mapfienlem3  7644  kmlem1  8307  fin1a2lem9  8565  nnind  10327  ublbneg  10926  supminf  10929  rlimrege0  13040  incexc2  13283  odcl  16018  odlem2  16021  gexcl  16058  gexlem2  16060  gexdvds  16062  pgpssslw  16092  resspsrmul  17422  mplbas2  17482  psropprmul  17590  coe1mul2  17620  psgnfix2  17870  psgndiflemB  17871  psgndif  17873  zrhcopsgndif  17874  txdis1cn  19049  ptcmplem3  19467  rrxmvallem  20744  mdegmullem  21433  0sgm  22366  sgmf  22367  sgmnncl  22369  dvdsdivcl  22405  fsumdvdsdiaglem  22407  fsumdvdscom  22409  dvdsppwf1o  22410  dvdsflf1o  22411  musumsum  22416  muinv  22417  sgmppw  22420  rpvmasumlem  22620  dchrmusum2  22627  dchrvmasumlem1  22628  dchrvmasum2lem  22629  dchrisum0fmul  22639  dchrisum0ff  22640  dchrisum0flblem1  22641  dchrisum0  22653  logsqvma  22675  usgraidx2v  23133  uvtxisvtx  23220  rabsnel  25710  nnindf  25911  ddemeas  26505  imambfm  26530  eulerpartlemgs2  26610  ballotlemfc0  26722  ballotlemfcc  26723  ballotlemirc  26761  mblfinlem2  28270  rencldnfilem  29001  irrapx1  29011  phisum  29409  stoweidlem15  29653  stoweidlem31  29669  elfvmptrab1  29997  elovmpt2rab  30001  elovmpt2rab1  30002  elovmpt3rab1  30006  2wlkonot3v  30237  2spthonot3v  30238  clwlkf1clwwlk  30366  frgrawopreglem4  30483  frgrawopreg  30485  bnj110  31550