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

Metamath Proof Explorer

Theorem inrab2

Description: Intersection with a restricted class abstraction. (Contributed by NM, 19-Nov-2007)

Ref Expression
Assertion inrab2 
|- ( { x e. A | ph } i^i B ) = { x e. ( A i^i B ) | ph }

Proof

Step Hyp Ref Expression
1 df-rab 
 |-  { x e. A | ph } = { x | ( x e. A /\ ph ) }
2 abid1 
 |-  B = { x | x e. B }
3 1 2 ineq12i 
 |-  ( { x e. A | ph } i^i B ) = ( { x | ( x e. A /\ ph ) } i^i { x | x e. B } )
4 df-rab 
 |-  { x e. ( A i^i B ) | ph } = { x | ( x e. ( A i^i B ) /\ ph ) }
5 inab 
 |-  ( { x | ( x e. A /\ ph ) } i^i { x | x e. B } ) = { x | ( ( x e. A /\ ph ) /\ x e. B ) }
6 elin 
 |-  ( x e. ( A i^i B ) <-> ( x e. A /\ x e. B ) )
7 6 anbi1i 
 |-  ( ( x e. ( A i^i B ) /\ ph ) <-> ( ( x e. A /\ x e. B ) /\ ph ) )
8 an32 
 |-  ( ( ( x e. A /\ x e. B ) /\ ph ) <-> ( ( x e. A /\ ph ) /\ x e. B ) )
9 7 8 bitri 
 |-  ( ( x e. ( A i^i B ) /\ ph ) <-> ( ( x e. A /\ ph ) /\ x e. B ) )
10 9 abbii 
 |-  { x | ( x e. ( A i^i B ) /\ ph ) } = { x | ( ( x e. A /\ ph ) /\ x e. B ) }
11 5 10 eqtr4i 
 |-  ( { x | ( x e. A /\ ph ) } i^i { x | x e. B } ) = { x | ( x e. ( A i^i B ) /\ ph ) }
12 4 11 eqtr4i 
 |-  { x e. ( A i^i B ) | ph } = ( { x | ( x e. A /\ ph ) } i^i { x | x e. B } )
13 3 12 eqtr4i 
 |-  ( { x e. A | ph } i^i B ) = { x e. ( A i^i B ) | ph }