Theorem elrabi 2917

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 2322	. . 3 |- ( A e. { x | ( x e. V /\ ph ) } <-> E. x ( x = A /\ ( x e. V /\ ph ) ) )
2		eleq1 2259	. . . . . 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 1612	. . 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 2484	. 2 |- { x e. V | ph } = { x | ( x e. V /\ ph ) }
8	6, 7	eleq2s 2291	1 |- ( A e. { x e. V | ph } -> A e. V )

Syntax hints:   -> wi 4   /\ wa 104   = wceq 1364   E.wex 1506   e. wcel 2167   {cab 2182   {crab 2479

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 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-11 1520  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-rab 2484

This theorem is referenced by:  ordtriexmidlem  4555  ordtri2or2exmidlem  4562  onsucelsucexmidlem  4565  ordsoexmid  4598  reg3exmidlemwe  4615  elfvmptrab1  5656  acexmidlemcase  5917  elovmporab  6123  elovmporab1w  6124  ssfirab  6997  exmidonfinlem  7260  cc4f  7336  genpelvl  7579  genpelvu  7580  suplocsrlempr  7874  nnindnn  7960  sup3exmid  8984  nnind  9006  supinfneg  9669  infsupneg  9670  supminfex  9671  ublbneg  9687  zsupcllemstep  10319  infssuzex  10323  infssuzledc  10324  hashinfuni  10869  bezoutlemsup  12176  uzwodc  12204  nninfctlemfo  12207  lcmgcdlem  12245  phisum  12409  oddennn  12609  evenennn  12610  znnen  12615  ennnfonelemg  12620  rrgval  13818  psrbagf  14224  txdis1cn  14514  reopnap  14782  divcnap  14801  limccl  14895  dvlemap  14916  dvaddxxbr  14937  dvmulxxbr  14938  dvcoapbr  14943  dvcjbr  14944  dvrecap  14949  dveflem  14962  sgmval  15219  0sgm  15221  sgmf  15222  sgmnncl  15224  dvdsppwf1o  15225  sgmppw  15228