Theorem elrabi 3251

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 2598	. . 3 |- ( A e. { x | ( x e. V /\ ph ) } <-> E. x ( x = A /\ ( x e. V /\ ph ) ) )
2		eleq1 2526	. . . . . 6 |- ( x = A -> ( x e. V <-> A e. V ) )
3	2	anbi1d 702	. . . . 5 |- ( x = A -> ( ( x e. V /\ ph ) <-> ( A e. V /\ ph ) ) )
4	3	simprbda 621	. . . 4 |- ( ( x = A /\ ( x e. V /\ ph ) ) -> A e. V )
5	4	exlimiv 1727	. . 3 |- ( E. x ( x = A /\ ( x e. V /\ ph ) ) -> A e. V )
6	1, 5	sylbi 195	. 2 |- ( A e. { x | ( x e. V /\ ph ) } -> A e. V )
7		df-rab 2813	. 2 |- { x e. V | ph } = { x | ( x e. V /\ ph ) }
8	6, 7	eleq2s 2562	1 |- ( A e. { x e. V | ph } -> A e. V )

Syntax hints:   -> wi 4   /\ wa 367   = wceq 1398   E.wex 1617   e. wcel 1823   {cab 2439   {crab 2808

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432

This theorem depends on definitions:  df-bi 185  df-an 369  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-rab 2813

This theorem is referenced by:  elfvmptrab1  5952  elovmpt2rab  6494  elovmpt2rab1  6495  elovmpt3rab1  6509  mapfienlem1  7856  mapfienlem2  7857  mapfienlem3  7858  kmlem1  8521  fin1a2lem9  8779  nnind  10549  ublbneg  11167  supminf  11170  rlimrege0  13484  incexc2  13732  isinitoi  15481  istermoi  15482  odcl  16759  odlem2  16762  gexcl  16799  gexlem2  16801  gexdvds  16803  pgpssslw  16833  resspsrmul  18267  mplbas2  18329  mptcoe1fsupp  18450  psropprmul  18474  coe1mul2  18505  psgnfix2  18808  psgndiflemB  18809  psgndif  18811  zrhcopsgndif  18812  cpmatpmat  19378  mptcoe1matfsupp  19470  mp2pm2mplem4  19477  chpscmat  19510  chpscmatgsumbin  19512  chpscmatgsummon  19513  txdis1cn  20302  ptcmplem3  20720  rrxmvallem  21997  mdegmullem  22644  0sgm  23616  sgmf  23617  sgmnncl  23619  dvdsdivcl  23655  fsumdvdsdiaglem  23657  fsumdvdscom  23659  dvdsppwf1o  23660  dvdsflf1o  23661  musumsum  23666  muinv  23667  sgmppw  23670  rpvmasumlem  23870  dchrmusum2  23877  dchrvmasumlem1  23878  dchrvmasum2lem  23879  dchrisum0fmul  23889  dchrisum0ff  23890  dchrisum0flblem1  23891  dchrisum0  23903  logsqvma  23925  usgraidx2v  24595  uvtxisvtx  24692  clwlkf1clwwlk  25052  2wlkonot3v  25077  2spthonot3v  25078  rusgranumwlks  25158  frgrawopreglem4  25249  frgrawopreg  25251  rabsnel  27601  nnindf  27844  ddemeas  28445  imambfm  28470  eulerpartlemgs2  28583  ballotlemfc0  28695  ballotlemfcc  28696  ballotlemirc  28734  mblfinlem2  30292  rencldnfilem  30993  irrapx1  31003  phisum  31400  radcnvrat  31436  lcmgcdlem  31453  dvnprodlem1  31982  stoweidlem15  32036  stoweidlem31  32052  fourierdlem25  32153  fourierdlem51  32179  fourierdlem79  32207  etransclem28  32284  usgresvm1  32815  usgresvm1ALT  32819  2zrngasgrp  33000  2zrngamnd  33001  2zrngacmnd  33002  2zrngagrp  33003  2zrngmsgrp  33007  2zrngALT  33008  2zrngnmlid  33009  2zrngnmlid2  33011  bnj110  34317