Theorem elrabi 2883

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 2296	. . 3 |- ( A e. { x | ( x e. V /\ ph ) } <-> E. x ( x = A /\ ( x e. V /\ ph ) ) )
2		eleq1 2233	. . . . . 6 |- ( x = A -> ( x e. V <-> A e. V ) )
3	2	anbi1d 462	. . . . 5 |- ( x = A -> ( ( x e. V /\ ph ) <-> ( A e. V /\ ph ) ) )
4	3	simprbda 381	. . . 4 |- ( ( x = A /\ ( x e. V /\ ph ) ) -> A e. V )
5	4	exlimiv 1591	. . 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 2457	. 2 |- { x e. V | ph } = { x | ( x e. V /\ ph ) }
8	6, 7	eleq2s 2265	1 |- ( A e. { x e. V | ph } -> A e. V )

Syntax hints:   -> wi 4   /\ wa 103   = wceq 1348   E.wex 1485   e. wcel 2141   {cab 2156   {crab 2452

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-11 1499  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-rab 2457

This theorem is referenced by:  ordtriexmidlem  4501  ordtri2or2exmidlem  4508  onsucelsucexmidlem  4511  ordsoexmid  4544  reg3exmidlemwe  4561  elfvmptrab1  5588  acexmidlemcase  5846  ssfirab  6908  exmidonfinlem  7159  cc4f  7220  genpelvl  7463  genpelvu  7464  suplocsrlempr  7758  nnindnn  7844  sup3exmid  8862  nnind  8883  supinfneg  9543  infsupneg  9544  supminfex  9545  ublbneg  9561  hashinfuni  10700  zsupcllemstep  11889  infssuzex  11893  infssuzledc  11894  bezoutlemsup  11953  uzwodc  11981  lcmgcdlem  12020  phisum  12183  oddennn  12336  evenennn  12337  znnen  12342  ennnfonelemg  12347  txdis1cn  13033  reopnap  13293  divcnap  13310  limccl  13383  dvlemap  13404  dvaddxxbr  13420  dvmulxxbr  13421  dvcoapbr  13426  dvcjbr  13427  dvrecap  13432  dveflem  13442