Theorem elintab 4487

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 4481	. 2 |- ( A e. |^| { x | ph } <-> A. y ( y e. { x | ph } -> A e. y ) )
3		nfsab1 2612	. . . 4 |- F/ x y e. { x | ph }
4		nfv 1843	. . . 4 |- F/ x A e. y
5	3, 4	nfim 1825	. . 3 |- F/ x ( y e. { x | ph } -> A e. y )
6		nfv 1843	. . 3 |- F/ y ( ph -> A e. x )
7		eleq1 2689	. . . . 5 |- ( y = x -> ( y e. { x | ph } <-> x e. { x | ph } ) )
8		abid 2610	. . . . 5 |- ( x e. { x | ph } <-> ph )
9	7, 8	syl6bb 276	. . . 4 |- ( y = x -> ( y e. { x | ph } <-> ph ) )
10		eleq2 2690	. . . 4 |- ( y = x -> ( A e. y <-> A e. x ) )
11	9, 10	imbi12d 334	. . 3 |- ( y = x -> ( ( y e. { x | ph } -> A e. y ) <-> ( ph -> A e. x ) ) )
12	5, 6, 11	cbval 2271	. 2 |- ( A. y ( y e. { x | ph } -> A e. y ) <-> A. x ( ph -> A e. x ) )
13	2, 12	bitri 264	1 |- ( A e. |^| { x | ph } <-> A. x ( ph -> A e. x ) )

Syntax hints:   -> wi 4   <-> wb 196   A.wal 1481   e. wcel 1990   {cab 2608   _Vcvv 3200   |^|cint 4475

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-int 4476

This theorem is referenced by:  elintrab  4488  intmin4  4506  intab  4507  intid  4926  dfom3  8544  dfom5  8547  tc2  8618  dfnn2  11033  brintclab  13742  efgi  18132  efgi2  18138  mclsax  31466  heibor1lem  33608  elmapintab  37902  intabssd  37916  cotrintab  37921  dffrege76  38233