Theorem intabs

Description: Absorption of a redundant conjunct in the intersection of a class abstraction. (Contributed by NM, 3-Jul-2005)

	Ref	Expression
Hypotheses	intabs.1	|- ( x = y -> ( ph <-> ps ) )
	intabs.2	|- ( x = |^| { y | ps } -> ( ph <-> ch ) )
	intabs.3	|- ( |^| { y | ps } C_ A /\ ch )
Assertion	intabs	|- |^| { x | ( x C_ A /\ ph ) } = |^| { x | ph }

Proof

Step	Hyp	Ref	Expression
1		intabs.1	|- ( x = y -> ( ph <-> ps ) )
2		intabs.2	|- ( x = |^| { y | ps } -> ( ph <-> ch ) )
3		intabs.3	|- ( |^| { y | ps } C_ A /\ ch )
4		sseq1	|- ( x = |^| { y | ps } -> ( x C_ A <-> |^| { y | ps } C_ A ) )
5	4 2	anbi12d	|- ( x = |^| { y | ps } -> ( ( x C_ A /\ ph ) <-> ( |^| { y | ps } C_ A /\ ch ) ) )
6	5 3	intmin3	|- ( |^| { y | ps } e. _V -> |^| { x | ( x C_ A /\ ph ) } C_ |^| { y | ps } )
7		intnex	|- ( -. |^| { y | ps } e. _V <-> |^| { y | ps } = _V )
8		ssv	|- |^| { x | ( x C_ A /\ ph ) } C_ _V
9		sseq2	|- ( |^| { y | ps } = _V -> ( |^| { x | ( x C_ A /\ ph ) } C_ |^| { y | ps } <-> |^| { x | ( x C_ A /\ ph ) } C_ _V ) )
10	8 9	mpbiri	|- ( |^| { y | ps } = _V -> |^| { x | ( x C_ A /\ ph ) } C_ |^| { y | ps } )
11	7 10	sylbi	|- ( -. |^| { y | ps } e. _V -> |^| { x | ( x C_ A /\ ph ) } C_ |^| { y | ps } )
12	6 11	pm2.61i	|- |^| { x | ( x C_ A /\ ph ) } C_ |^| { y | ps }
13	1	cbvabv	|- { x | ph } = { y | ps }
14	13	inteqi	|- |^| { x | ph } = |^| { y | ps }
15	12 14	sseqtrri	|- |^| { x | ( x C_ A /\ ph ) } C_ |^| { x | ph }
16		simpr	|- ( ( x C_ A /\ ph ) -> ph )
17	16	ss2abi	|- { x | ( x C_ A /\ ph ) } C_ { x | ph }
18		intss	|- ( { x | ( x C_ A /\ ph ) } C_ { x | ph } -> |^| { x | ph } C_ |^| { x | ( x C_ A /\ ph ) } )
19	17 18	ax-mp	|- |^| { x | ph } C_ |^| { x | ( x C_ A /\ ph ) }
20	15 19	eqssi	|- |^| { x | ( x C_ A /\ ph ) } = |^| { x | ph }