Theorem elrabi 3195

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 2578	. . 3 |- ( A e. { x | ( x e. V /\ ph ) } <-> E. x ( x = A /\ ( x e. V /\ ph ) ) )
2		eleq1 2519	. . . . . 6 |- ( x = A -> ( x e. V <-> A e. V ) )
3	2	anbi1d 712	. . . . 5 |- ( x = A -> ( ( x e. V /\ ph ) <-> ( A e. V /\ ph ) ) )
4	3	simprbda 629	. . . 4 |- ( ( x = A /\ ( x e. V /\ ph ) ) -> A e. V )
5	4	exlimiv 1778	. . 3 |- ( E. x ( x = A /\ ( x e. V /\ ph ) ) -> A e. V )
6	1, 5	sylbi 199	. 2 |- ( A e. { x | ( x e. V /\ ph ) } -> A e. V )
7		df-rab 2748	. 2 |- { x e. V | ph } = { x | ( x e. V /\ ph ) }
8	6, 7	eleq2s 2549	1 |- ( A e. { x e. V | ph } -> A e. V )

Syntax hints:   -> wi 4   /\ wa 371   = wceq 1446   E.wex 1665   e. wcel 1889   {cab 2439   {crab 2743

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1671  ax-4 1684  ax-5 1760  ax-6 1807  ax-7 1853  ax-10 1917  ax-11 1922  ax-12 1935  ax-13 2093  ax-ext 2433

This theorem depends on definitions:  df-bi 189  df-an 373  df-ex 1666  df-nf 1670  df-sb 1800  df-clab 2440  df-cleq 2446  df-clel 2449  df-rab 2748

This theorem is referenced by:  elfvmptrab1  5975  elovmpt2rab  6520  elovmpt2rab1  6521  elovmpt3rab1  6532  mapfienlem1  7923  mapfienlem2  7924  mapfienlem3  7925  kmlem1  8585  fin1a2lem9  8843  nnind  10634  ublbneg  11255  supminf  11257  supminfOLD  11258  rlimrege0  13655  incexc2  13908  lcmgcdlem  14583  prmgaplem5  15037  isinitoi  15910  istermoi  15911  odcl  17197  odlem2  17200  odclOLD  17213  odlem2OLD  17216  gexcl  17243  gexlem2  17245  gexdvds  17247  gexlem2OLD  17248  pgpssslw  17278  resspsrmul  18653  mplbas2  18706  mptcoe1fsupp  18820  psropprmul  18843  coe1mul2  18874  psgnfix2  19179  psgndiflemB  19180  psgndif  19182  zrhcopsgndif  19183  cpmatpmat  19746  mptcoe1matfsupp  19838  mp2pm2mplem4  19845  chpscmat  19878  chpscmatgsumbin  19880  chpscmatgsummon  19881  txdis1cn  20662  ptcmplem3  21081  rrxmvallem  22370  mdegmullem  23039  0sgm  24083  sgmf  24084  sgmnncl  24086  dvdsdivcl  24122  fsumdvdsdiaglem  24124  fsumdvdscom  24126  dvdsppwf1o  24127  dvdsflf1o  24128  musumsum  24133  muinv  24134  sgmppw  24137  rpvmasumlem  24337  dchrmusum2  24344  dchrvmasumlem1  24345  dchrvmasum2lem  24346  dchrisum0fmul  24356  dchrisum0ff  24357  dchrisum0flblem1  24358  dchrisum0  24370  logsqvma  24392  usgraidx2v  25132  uvtxisvtx  25230  clwlkf1clwwlk  25590  2wlkonot3v  25615  2spthonot3v  25616  rusgranumwlks  25696  frgrawopreglem4  25787  frgrawopreg  25789  rabsnel  28150  nnindf  28394  ddemeas  29071  imambfm  29096  eulerpartlemgs2  29225  ballotlemfc0  29337  ballotlemfcc  29338  ballotlemirc  29376  ballotlemircOLD  29414  bnj110  29681  poimirlem4  31956  poimirlem5  31957  poimirlem6  31958  poimirlem7  31959  poimirlem8  31960  poimirlem9  31961  poimirlem10  31962  poimirlem11  31963  poimirlem12  31964  poimirlem13  31965  poimirlem14  31966  poimirlem15  31967  poimirlem16  31968  poimirlem17  31969  poimirlem18  31970  poimirlem19  31971  poimirlem20  31972  poimirlem21  31973  poimirlem22  31974  poimirlem26  31978  mblfinlem2  31990  rencldnfilem  35675  irrapx1  35684  phisum  36088  radcnvrat  36674  fsumiunss  37664  dvnprodlem1  37831  stoweidlem15  37885  stoweidlem31  37902  fourierdlem25  38004  fourierdlem51  38031  fourierdlem79  38059  etransclem28  38137  issalgend  38207  sge0iunmptlemre  38267  hoidmvlelem2  38428  usgredg2v  39314  umgrres1lem  39387  upgrres1  39390  uvtxaisvtx  39471  usgresvm1  39859  usgresvm1ALT  39863  2zrngasgrp  40044  2zrngamnd  40045  2zrngacmnd  40046  2zrngagrp  40047  2zrngmsgrp  40051  2zrngALT  40052  2zrngnmlid  40053  2zrngnmlid2  40055