Theorem elrabi 2884

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 2297	. . 3 |- ( A e. { x | ( x e. V /\ ph ) } <-> E. x ( x = A /\ ( x e. V /\ ph ) ) )
2		eleq1 2234	. . . . . 6 |- ( x = A -> ( x e. V <-> A e. V ) )
3	2	anbi1d 463	. . . . 5 |- ( x = A -> ( ( x e. V /\ ph ) <-> ( A e. V /\ ph ) ) )
4	3	simprbda 381	. . . 4 |- ( ( x = A /\ ( x e. V /\ ph ) ) -> A e. V )
5	4	exlimiv 1592	. . 3 |- ( E. x ( x = A /\ ( x e. V /\ ph ) ) -> A e. V )
6	1, 5	sylbi 120	. 2 |- ( A e. { x | ( x e. V /\ ph ) } -> A e. V )
7		df-rab 2458	. 2 |- { x e. V | ph } = { x | ( x e. V /\ ph ) }
8	6, 7	eleq2s 2266	1 |- ( A e. { x e. V | ph } -> A e. V )

Syntax hints:   -> wi 4   /\ wa 103   = wceq 1349   E.wex 1486   e. wcel 2142   {cab 2157   {crab 2453

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1441  ax-7 1442  ax-gen 1443  ax-ie1 1487  ax-ie2 1488  ax-8 1498  ax-11 1500  ax-4 1504  ax-17 1520  ax-i9 1524  ax-ial 1528  ax-ext 2153

This theorem depends on definitions:  df-bi 116  df-nf 1455  df-sb 1757  df-clab 2158  df-cleq 2164  df-clel 2167  df-rab 2458

This theorem is referenced by:  ordtriexmidlem  4504  ordtri2or2exmidlem  4511  onsucelsucexmidlem  4514  ordsoexmid  4547  reg3exmidlemwe  4564  elfvmptrab1  5594  acexmidlemcase  5852  ssfirab  6915  exmidonfinlem  7174  cc4f  7235  genpelvl  7478  genpelvu  7479  suplocsrlempr  7773  nnindnn  7859  sup3exmid  8877  nnind  8898  supinfneg  9558  infsupneg  9559  supminfex  9560  ublbneg  9576  hashinfuni  10715  zsupcllemstep  11904  infssuzex  11908  infssuzledc  11909  bezoutlemsup  11968  uzwodc  11996  lcmgcdlem  12035  phisum  12198  oddennn  12351  evenennn  12352  znnen  12357  ennnfonelemg  12362  txdis1cn  13157  reopnap  13417  divcnap  13434  limccl  13507  dvlemap  13528  dvaddxxbr  13544  dvmulxxbr  13545  dvcoapbr  13550  dvcjbr  13551  dvrecap  13556  dveflem  13566