Metamath Proof Explorer


Theorem bj-inrab

Description: Generalization of inrab . (Contributed by BJ, 21-Apr-2019)

Ref Expression
Assertion bj-inrab
|- ( { x e. A | ph } i^i { x e. B | ps } ) = { x e. ( A i^i B ) | ( ph /\ ps ) }

Proof

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