This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 }