Theorem elintab 4237

Description: Membership in the intersection of a class abstraction. (Contributed by NM, 30-Aug-1993.)

Hypothesis

Ref	Expression
inteqab.1	|- A e. _V

Assertion

Ref	Expression
elintab	|- ( A e. |^| { x | ph } <-> A. x ( ph -> A e. x ) )

Distinct variable group:   x, A

Allowed substitution hint:   ph( x)

Proof of Theorem elintab

Dummy variable y is distinct from all other variables.

Step	Hyp	Ref	Expression
1		inteqab.1	. . 3 |- A e. _V
2	1	elint 4232	. 2 |- ( A e. |^| { x | ph } <-> A. y ( y e. { x | ph } -> A e. y ) )
3		nfsab1 2461	. . . 4 |- F/ x y e. { x | ph }
4		nfv 1769	. . . 4 |- F/ x A e. y
5	3, 4	nfim 2023	. . 3 |- F/ x ( y e. { x | ph } -> A e. y )
6		nfv 1769	. . 3 |- F/ y ( ph -> A e. x )
7		eleq1 2537	. . . . 5 |- ( y = x -> ( y e. { x | ph } <-> x e. { x | ph } ) )
8		abid 2459	. . . . 5 |- ( x e. { x | ph } <-> ph )
9	7, 8	syl6bb 269	. . . 4 |- ( y = x -> ( y e. { x | ph } <-> ph ) )
10		eleq2 2538	. . . 4 |- ( y = x -> ( A e. y <-> A e. x ) )
11	9, 10	imbi12d 327	. . 3 |- ( y = x -> ( ( y e. { x | ph } -> A e. y ) <-> ( ph -> A e. x ) ) )
12	5, 6, 11	cbval 2127	. 2 |- ( A. y ( y e. { x | ph } -> A e. y ) <-> A. x ( ph -> A e. x ) )
13	2, 12	bitri 257	1 |- ( A e. |^| { x | ph } <-> A. x ( ph -> A e. x ) )

Syntax hints:   -> wi 4   <-> wb 189   A.wal 1450   e. wcel 1904   {cab 2457   _Vcvv 3031   |^|cint 4226

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451

This theorem depends on definitions:  df-bi 190  df-an 378  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-v 3033  df-int 4227

This theorem is referenced by:  elintrab  4238  intmin4  4255  intab  4256  intid  4658  dfom3  8170  dfom5  8173  tc2  8244  dfnn2  10644  brintclab  13142  efgi  17447  efgi2  17453  mclsax  30279  heibor1lem  32205  elmapintab  36273  intabssd  36287  cotrintab  36292  dffrege76  36606