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  5731  acexmidlemcase  6002  elovmporab  6211  elovmporab1w  6212  ssfirab  7109  exmidonfinlem  7382  cc4f  7466  genpelvl  7710  genpelvu  7711  suplocsrlempr  8005  nnindnn  8091  sup3exmid  9115  nnind  9137  supinfneg  9802  infsupneg  9803  supminfex  9804  ublbneg  9820  zsupcllemstep  10461  infssuzex  10465  infssuzledc  10466  hashinfuni  11011  bezoutlemsup  12546  uzwodc  12574  nninfctlemfo  12577  lcmgcdlem  12615  phisum  12779  oddennn  12979  evenennn  12980  znnen  12985  ennnfonelemg  12990  rrgval  14242  psrbagf  14650  txdis1cn  14968  reopnap  15236  divcnap  15255  limccl  15349  dvlemap  15370  dvaddxxbr  15391  dvmulxxbr  15392  dvcoapbr  15397  dvcjbr  15398  dvrecap  15403  dveflem  15416  sgmval  15673  0sgm  15675  sgmf  15676  sgmnncl  15678  dvdsppwf1o  15679  sgmppw  15682  uhgrss  15891  usgredg2v  16038