Theorem elrabi 2804

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 2237	. . 3 |- ( A e. { x | ( x e. V /\ ph ) } <-> E. x ( x = A /\ ( x e. V /\ ph ) ) )
2		eleq1 2175	. . . . . 6 |- ( x = A -> ( x e. V <-> A e. V ) )
3	2	anbi1d 458	. . . . 5 |- ( x = A -> ( ( x e. V /\ ph ) <-> ( A e. V /\ ph ) ) )
4	3	simprbda 378	. . . 4 |- ( ( x = A /\ ( x e. V /\ ph ) ) -> A e. V )
5	4	exlimiv 1558	. . 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 2397	. 2 |- { x e. V | ph } = { x | ( x e. V /\ ph ) }
8	6, 7	eleq2s 2207	1 |- ( A e. { x e. V | ph } -> A e. V )

Syntax hints:   -> wi 4   /\ wa 103   = wceq 1312   E.wex 1449   e. wcel 1461   {cab 2099   {crab 2392

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1404  ax-7 1405  ax-gen 1406  ax-ie1 1450  ax-ie2 1451  ax-8 1463  ax-11 1465  ax-4 1468  ax-17 1487  ax-i9 1491  ax-ial 1495  ax-ext 2095

This theorem depends on definitions:  df-bi 116  df-nf 1418  df-sb 1717  df-clab 2100  df-cleq 2106  df-clel 2109  df-rab 2397

This theorem is referenced by:  ordtriexmidlem  4393  ordtri2or2exmidlem  4399  onsucelsucexmidlem  4402  ordsoexmid  4435  reg3exmidlemwe  4451  elfvmptrab1  5467  acexmidlemcase  5721  ssfirab  6771  genpelvl  7261  genpelvu  7262  nnindnn  7621  sup3exmid  8618  nnind  8639  supinfneg  9285  infsupneg  9286  supminfex  9287  ublbneg  9300  hashinfuni  10409  zsupcllemstep  11479  infssuzex  11483  infssuzledc  11484  bezoutlemsup  11536  lcmgcdlem  11597  oddennn  11743  evenennn  11744  znnen  11749  ennnfonelemg  11754  txdis1cn  12282  divcnap  12534  limccl  12577  dvlemap  12597