Theorem elrabi 2960

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 2358	. . 3 |- ( A e. { x | ( x e. V /\ ph ) } <-> E. x ( x = A /\ ( x e. V /\ ph ) ) )
2		eleq1 2294	. . . . . 6 |- ( x = A -> ( x e. V <-> A e. V ) )
3	2	anbi1d 465	. . . . 5 |- ( x = A -> ( ( x e. V /\ ph ) <-> ( A e. V /\ ph ) ) )
4	3	simprbda 383	. . . 4 |- ( ( x = A /\ ( x e. V /\ ph ) ) -> A e. V )
5	4	exlimiv 1647	. . 3 |- ( E. x ( x = A /\ ( x e. V /\ ph ) ) -> A e. V )
6	1, 5	sylbi 121	. 2 |- ( A e. { x | ( x e. V /\ ph ) } -> A e. V )
7		df-rab 2520	. 2 |- { x e. V | ph } = { x | ( x e. V /\ ph ) }
8	6, 7	eleq2s 2326	1 |- ( A e. { x e. V | ph } -> A e. V )

Syntax hints:   -> wi 4   /\ wa 104   = wceq 1398   E.wex 1541   e. wcel 2202   {cab 2217   {crab 2515

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-11 1555  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-rab 2520

This theorem is referenced by:  rabsnif  3742  ordtriexmidlem  4623  ordtri2or2exmidlem  4630  onsucelsucexmidlem  4633  ordsoexmid  4666  reg3exmidlemwe  4683  elfvmptrab1  5750  acexmidlemcase  6023  elovmporab  6232  elovmporab1w  6233  ssfirab  7172  exmidonfinlem  7464  cc4f  7548  genpelvl  7792  genpelvu  7793  suplocsrlempr  8087  nnindnn  8173  sup3exmid  9196  nnind  9218  supinfneg  9890  infsupneg  9891  supminfex  9892  ublbneg  9908  zsupcllemstep  10552  infssuzex  10556  infssuzledc  10557  hashinfuni  11102  bezoutlemsup  12660  uzwodc  12688  nninfctlemfo  12691  lcmgcdlem  12729  phisum  12893  oddennn  13093  evenennn  13094  znnen  13099  ennnfonelemg  13104  rrgval  14357  psrbagf  14766  txdis1cn  15089  reopnap  15357  divcnap  15376  limccl  15470  dvlemap  15491  dvaddxxbr  15512  dvmulxxbr  15513  dvcoapbr  15518  dvcjbr  15519  dvrecap  15524  dveflem  15537  sgmval  15797  0sgm  15799  sgmf  15800  sgmnncl  15802  dvdsppwf1o  15803  sgmppw  15806  uhgrss  16016  usgredg2v  16165  subumgredg2en  16212  clwwlknon  16370