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  9251  nnind  9273  supinfneg  9948  infsupneg  9949  supminfex  9950  ublbneg  9966  zsupcllemstep  10614  infssuzex  10618  infssuzledc  10619  hashinfuni  11168  bezoutlemsup  12733  uzwodc  12761  nninfctlemfo  12764  lcmgcdlem  12802  phisum  12966  ballotfilemfc0  13179  ballotfilemfcc  13180  ballotfilemfrcn0  13220  ballotfilemirc  13222  oddennn  13230  evenennn  13231  znnen  13236  ennnfonelemg  13241  rrgval  14511  psrbagf  14947  txdis1cn  15272  reopnap  15540  divcnap  15559  limccl  15653  dvlemap  15674  dvaddxxbr  15695  dvmulxxbr  15696  dvcoapbr  15701  dvcjbr  15702  dvrecap  15707  dveflem  15720  sgmval  15980  0sgm  15982  sgmf  15983  sgmnncl  15985  dvdsppwf1o  15986  sgmppw  15989  uhgrss  16199  usgredg2v  16348  subumgredg2en  16395  clwwlknon  16553