Metamath Proof Explorer


Theorem bj-inrab3

Description: Generalization of dfrab3ss , which it may shorten. (Contributed by BJ, 21-Apr-2019) (Revised by OpenAI, 7-Jul-2020)

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

Proof

Step Hyp Ref Expression
1 dfrab3
 |-  { x e. B | ph } = ( B i^i { x | ph } )
2 1 ineq2i
 |-  ( A i^i { x e. B | ph } ) = ( A i^i ( B i^i { x | ph } ) )
3 dfrab3
 |-  { x e. A | ph } = ( A i^i { x | ph } )
4 3 ineq2i
 |-  ( B i^i { x e. A | ph } ) = ( B i^i ( A i^i { x | ph } ) )
5 incom
 |-  ( { x e. A | ph } i^i B ) = ( B i^i { x e. A | ph } )
6 in12
 |-  ( A i^i ( B i^i { x | ph } ) ) = ( B i^i ( A i^i { x | ph } ) )
7 4 5 6 3eqtr4i
 |-  ( { x e. A | ph } i^i B ) = ( A i^i ( B i^i { x | ph } ) )
8 2 7 eqtr4i
 |-  ( A i^i { x e. B | ph } ) = ( { x e. A | ph } i^i B )