Theorem elrabi 2905

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 2315	. . 3 |- ( A e. { x | ( x e. V /\ ph ) } <-> E. x ( x = A /\ ( x e. V /\ ph ) ) )
2		eleq1 2252	. . . . . 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 1609	. . 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 2477	. 2 |- { x e. V | ph } = { x | ( x e. V /\ ph ) }
8	6, 7	eleq2s 2284	1 |- ( A e. { x e. V | ph } -> A e. V )

Syntax hints:   -> wi 4   /\ wa 104   = wceq 1364   E.wex 1503   e. wcel 2160   {cab 2175   {crab 2472

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 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-11 1517  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-ext 2171

This theorem depends on definitions:  df-bi 117  df-nf 1472  df-sb 1774  df-clab 2176  df-cleq 2182  df-clel 2185  df-rab 2477

This theorem is referenced by:  ordtriexmidlem  4536  ordtri2or2exmidlem  4543  onsucelsucexmidlem  4546  ordsoexmid  4579  reg3exmidlemwe  4596  elfvmptrab1  5630  acexmidlemcase  5890  ssfirab  6961  exmidonfinlem  7221  cc4f  7297  genpelvl  7540  genpelvu  7541  suplocsrlempr  7835  nnindnn  7921  sup3exmid  8943  nnind  8964  supinfneg  9624  infsupneg  9625  supminfex  9626  ublbneg  9642  hashinfuni  10788  zsupcllemstep  11977  infssuzex  11981  infssuzledc  11982  bezoutlemsup  12041  uzwodc  12069  lcmgcdlem  12108  phisum  12271  oddennn  12442  evenennn  12443  znnen  12448  ennnfonelemg  12453  psrbagf  13945  txdis1cn  14230  reopnap  14490  divcnap  14507  limccl  14580  dvlemap  14601  dvaddxxbr  14617  dvmulxxbr  14618  dvcoapbr  14623  dvcjbr  14624  dvrecap  14629  dveflem  14639