Theorem elrabi 2973

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 2362	. . 3 |- ( A e. { x | ( x e. V /\ ph ) } <-> E. x ( x = A /\ ( x e. V /\ ph ) ) )
2		eleq1 2297	. . . . . 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 1647	. . 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 2531	. 2 |- { x e. V | ph } = { x | ( x e. V /\ ph ) }
8	6, 7	eleq2s 2329	1 |- ( A e. { x e. V | ph } -> A e. V )

Syntax hints:   -> wi 4   /\ wa 104   = wceq 1398   E.wex 1541   e. wcel 2205   {cab 2220   {crab 2526

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 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-11 1555  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-rab 2531

This theorem is referenced by:  rabsnif  3763  ordtriexmidlem  4646  ordtri2or2exmidlem  4653  onsucelsucexmidlem  4656  ordsoexmid  4689  reg3exmidlemwe  4706  elfvmptrab1  5777  acexmidlemcase  6053  elovmporab  6262  elovmporab1w  6263  ssfirab  7210  exmidonfinlem  7509  cc4f  7599  genpelvl  7843  genpelvu  7844  suplocsrlempr  8138  nnindnn  8224  sup3exmid  9248  nnind  9270  supinfneg  9945  infsupneg  9946  supminfex  9947  ublbneg  9963  zsupcllemstep  10611  infssuzex  10615  infssuzledc  10616  hashinfuni  11165  bezoutlemsup  12730  uzwodc  12758  nninfctlemfo  12761  lcmgcdlem  12799  phisum  12963  ballotfilemfc0  13176  ballotfilemfcc  13177  ballotfilemfrcn0  13217  ballotfilemirc  13219  oddennn  13227  evenennn  13228  znnen  13233  ennnfonelemg  13238  rrgval  14508  psrbagf  14944  txdis1cn  15269  reopnap  15537  divcnap  15556  limccl  15650  dvlemap  15671  dvaddxxbr  15692  dvmulxxbr  15693  dvcoapbr  15698  dvcjbr  15699  dvrecap  15704  dveflem  15717  sgmval  15977  0sgm  15979  sgmf  15980  sgmnncl  15982  dvdsppwf1o  15983  sgmppw  15986  uhgrss  16196  usgredg2v  16345  subumgredg2en  16392  clwwlknon  16550