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 }