Theorem elrabi 2956

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 2355	. . 3 |- ( A e. { x | ( x e. V /\ ph ) } <-> E. x ( x = A /\ ( x e. V /\ ph ) ) )
2		eleq1 2292	. . . . . 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 1644	. . 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 2517	. 2 |- { x e. V | ph } = { x | ( x e. V /\ ph ) }
8	6, 7	eleq2s 2324	1 |- ( A e. { x e. V | ph } -> A e. V )

Syntax hints:   -> wi 4   /\ wa 104   = wceq 1395   E.wex 1538   e. wcel 2200   {cab 2215   {crab 2512

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 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-11 1552  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-rab 2517

This theorem is referenced by:  ordtriexmidlem  4611  ordtri2or2exmidlem  4618  onsucelsucexmidlem  4621  ordsoexmid  4654  reg3exmidlemwe  4671  elfvmptrab1  5729  acexmidlemcase  5996  elovmporab  6205  elovmporab1w  6206  ssfirab  7098  exmidonfinlem  7371  cc4f  7455  genpelvl  7699  genpelvu  7700  suplocsrlempr  7994  nnindnn  8080  sup3exmid  9104  nnind  9126  supinfneg  9790  infsupneg  9791  supminfex  9792  ublbneg  9808  zsupcllemstep  10449  infssuzex  10453  infssuzledc  10454  hashinfuni  10999  bezoutlemsup  12530  uzwodc  12558  nninfctlemfo  12561  lcmgcdlem  12599  phisum  12763  oddennn  12963  evenennn  12964  znnen  12969  ennnfonelemg  12974  rrgval  14226  psrbagf  14634  txdis1cn  14952  reopnap  15220  divcnap  15239  limccl  15333  dvlemap  15354  dvaddxxbr  15375  dvmulxxbr  15376  dvcoapbr  15381  dvcjbr  15382  dvrecap  15387  dveflem  15400  sgmval  15657  0sgm  15659  sgmf  15660  sgmnncl  15662  dvdsppwf1o  15663  sgmppw  15666  uhgrss  15875  usgredg2v  16022