Theorem elrabi 3226

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 2566	. . 3 |- ( A e. { x | ( x e. V /\ ph ) } <-> E. x ( x = A /\ ( x e. V /\ ph ) ) )
2		eleq1 2494	. . . . . 6 |- ( x = A -> ( x e. V <-> A e. V ) )
3	2	anbi1d 709	. . . . 5 |- ( x = A -> ( ( x e. V /\ ph ) <-> ( A e. V /\ ph ) ) )
4	3	simprbda 627	. . . 4 |- ( ( x = A /\ ( x e. V /\ ph ) ) -> A e. V )
5	4	exlimiv 1766	. . 3 |- ( E. x ( x = A /\ ( x e. V /\ ph ) ) -> A e. V )
6	1, 5	sylbi 198	. 2 |- ( A e. { x | ( x e. V /\ ph ) } -> A e. V )
7		df-rab 2784	. 2 |- { x e. V | ph } = { x | ( x e. V /\ ph ) }
8	6, 7	eleq2s 2530	1 |- ( A e. { x e. V | ph } -> A e. V )

Syntax hints:   -> wi 4   /\ wa 370   = wceq 1437   E.wex 1659   e. wcel 1868   {cab 2407   {crab 2779

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400

This theorem depends on definitions:  df-bi 188  df-an 372  df-ex 1660  df-nf 1664  df-sb 1787  df-clab 2408  df-cleq 2414  df-clel 2417  df-rab 2784

This theorem is referenced by:  elfvmptrab1  5983  elovmpt2rab  6526  elovmpt2rab1  6527  elovmpt3rab1  6538  mapfienlem1  7921  mapfienlem2  7922  mapfienlem3  7923  kmlem1  8581  fin1a2lem9  8839  nnind  10628  ublbneg  11249  supminf  11251  supminfOLD  11252  rlimrege0  13631  incexc2  13884  lcmgcdlem  14559  prmgaplem5  15013  isinitoi  15886  istermoi  15887  odcl  17173  odlem2  17176  odclOLD  17189  odlem2OLD  17192  gexcl  17219  gexlem2  17221  gexdvds  17223  gexlem2OLD  17224  pgpssslw  17254  resspsrmul  18629  mplbas2  18682  mptcoe1fsupp  18796  psropprmul  18819  coe1mul2  18850  psgnfix2  19154  psgndiflemB  19155  psgndif  19157  zrhcopsgndif  19158  cpmatpmat  19721  mptcoe1matfsupp  19813  mp2pm2mplem4  19820  chpscmat  19853  chpscmatgsumbin  19855  chpscmatgsummon  19856  txdis1cn  20637  ptcmplem3  21056  rrxmvallem  22345  mdegmullem  23014  0sgm  24058  sgmf  24059  sgmnncl  24061  dvdsdivcl  24097  fsumdvdsdiaglem  24099  fsumdvdscom  24101  dvdsppwf1o  24102  dvdsflf1o  24103  musumsum  24108  muinv  24109  sgmppw  24112  rpvmasumlem  24312  dchrmusum2  24319  dchrvmasumlem1  24320  dchrvmasum2lem  24321  dchrisum0fmul  24331  dchrisum0ff  24332  dchrisum0flblem1  24333  dchrisum0  24345  logsqvma  24367  usgraidx2v  25107  uvtxisvtx  25204  clwlkf1clwwlk  25564  2wlkonot3v  25589  2spthonot3v  25590  rusgranumwlks  25670  frgrawopreglem4  25761  frgrawopreg  25763  rabsnel  28125  nnindf  28377  ddemeas  29055  imambfm  29080  eulerpartlemgs2  29209  ballotlemfc0  29321  ballotlemfcc  29322  ballotlemirc  29360  ballotlemircOLD  29398  bnj110  29665  poimirlem4  31858  poimirlem5  31859  poimirlem6  31860  poimirlem7  31861  poimirlem8  31862  poimirlem9  31863  poimirlem10  31864  poimirlem11  31865  poimirlem12  31866  poimirlem13  31867  poimirlem14  31868  poimirlem15  31869  poimirlem16  31870  poimirlem17  31871  poimirlem18  31872  poimirlem19  31873  poimirlem20  31874  poimirlem21  31875  poimirlem22  31876  poimirlem26  31880  mblfinlem2  31892  rencldnfilem  35582  irrapx1  35592  phisum  35996  radcnvrat  36521  fsumiunss  37477  dvnprodlem1  37641  stoweidlem15  37695  stoweidlem31  37712  fourierdlem25  37814  fourierdlem51  37841  fourierdlem79  37869  etransclem28  37947  sge0iunmptlemre  38045  usgridx2v  38930  usgresvm1  39027  usgresvm1ALT  39031  2zrngasgrp  39212  2zrngamnd  39213  2zrngacmnd  39214  2zrngagrp  39215  2zrngmsgrp  39219  2zrngALT  39220  2zrngnmlid  39221  2zrngnmlid2  39223