Theorem elrabi 3113

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 2562	. . 3 |- ( A e. { x | ( x e. V /\ ph ) } <-> E. x ( x = A /\ ( x e. V /\ ph ) ) )
2		eleq1 2502	. . . . . 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 1688	. . 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 2723	. 2 |- { x e. V | ph } = { x | ( x e. V /\ ph ) }
8	6, 7	eleq2s 2534	1 |- ( A e. { x e. V | ph } -> A e. V )

Syntax hints:   -> wi 4   /\ wa 369   = wceq 1369   E.wex 1586   e. wcel 1756   {cab 2428   {crab 2718

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2429  df-cleq 2435  df-clel 2438  df-rab 2723

This theorem is referenced by:  mapfienlem1  7653  mapfienlem2  7654  mapfienlem3  7655  kmlem1  8318  fin1a2lem9  8576  nnind  10339  ublbneg  10938  supminf  10941  rlimrege0  13056  incexc2  13300  odcl  16038  odlem2  16041  gexcl  16078  gexlem2  16080  gexdvds  16082  pgpssslw  16112  resspsrmul  17488  mplbas2  17550  psropprmul  17692  coe1mul2  17722  psgnfix2  18028  psgndiflemB  18029  psgndif  18031  zrhcopsgndif  18032  txdis1cn  19207  ptcmplem3  19625  rrxmvallem  20902  mdegmullem  21548  0sgm  22481  sgmf  22482  sgmnncl  22484  dvdsdivcl  22520  fsumdvdsdiaglem  22522  fsumdvdscom  22524  dvdsppwf1o  22525  dvdsflf1o  22526  musumsum  22531  muinv  22532  sgmppw  22535  rpvmasumlem  22735  dchrmusum2  22742  dchrvmasumlem1  22743  dchrvmasum2lem  22744  dchrisum0fmul  22754  dchrisum0ff  22755  dchrisum0flblem1  22756  dchrisum0  22768  logsqvma  22790  usgraidx2v  23310  uvtxisvtx  23397  rabsnel  25886  nnindf  26088  ddemeas  26651  imambfm  26676  eulerpartlemgs2  26762  ballotlemfc0  26874  ballotlemfcc  26875  ballotlemirc  26913  mblfinlem2  28427  rencldnfilem  29157  irrapx1  29167  phisum  29565  stoweidlem15  29808  stoweidlem31  29824  elfvmptrab1  30152  elovmpt2rab  30156  elovmpt2rab1  30157  elovmpt3rab1  30161  2wlkonot3v  30392  2spthonot3v  30393  clwlkf1clwwlk  30521  frgrawopreglem4  30638  frgrawopreg  30640  mptcoe1fsupp  30831  dmatmul  30874  dmatsubcl  30875  dmatmulcl  30877  dmatcrng  30879  scmatsubcl  30882  scmatmulcl  30884  scmatcrng  30886  mptcoe1matfsupp  30889  mp2pm2mplem4  30917  bnj110  31849