Theorem elrabi 2926

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 2331	. . 3 |- ( A e. { x | ( x e. V /\ ph ) } <-> E. x ( x = A /\ ( x e. V /\ ph ) ) )
2		eleq1 2268	. . . . . 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 1621	. . 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 2493	. 2 |- { x e. V | ph } = { x | ( x e. V /\ ph ) }
8	6, 7	eleq2s 2300	1 |- ( A e. { x e. V | ph } -> A e. V )

Syntax hints:   -> wi 4   /\ wa 104   = wceq 1373   E.wex 1515   e. wcel 2176   {cab 2191   {crab 2488

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 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-11 1529  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-rab 2493

This theorem is referenced by:  ordtriexmidlem  4568  ordtri2or2exmidlem  4575  onsucelsucexmidlem  4578  ordsoexmid  4611  reg3exmidlemwe  4628  elfvmptrab1  5676  acexmidlemcase  5941  elovmporab  6148  elovmporab1w  6149  ssfirab  7035  exmidonfinlem  7303  cc4f  7383  genpelvl  7627  genpelvu  7628  suplocsrlempr  7922  nnindnn  8008  sup3exmid  9032  nnind  9054  supinfneg  9718  infsupneg  9719  supminfex  9720  ublbneg  9736  zsupcllemstep  10374  infssuzex  10378  infssuzledc  10379  hashinfuni  10924  bezoutlemsup  12363  uzwodc  12391  nninfctlemfo  12394  lcmgcdlem  12432  phisum  12596  oddennn  12796  evenennn  12797  znnen  12802  ennnfonelemg  12807  rrgval  14057  psrbagf  14465  txdis1cn  14783  reopnap  15051  divcnap  15070  limccl  15164  dvlemap  15185  dvaddxxbr  15206  dvmulxxbr  15207  dvcoapbr  15212  dvcjbr  15213  dvrecap  15218  dveflem  15231  sgmval  15488  0sgm  15490  sgmf  15491  sgmnncl  15493  dvdsppwf1o  15494  sgmppw  15497