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 x B | φ = x A | φ B

Proof

Step Hyp Ref Expression
1 dfrab3 x B | φ = B x | φ
2 1 ineq2i A x B | φ = A B x | φ
3 dfrab3 x A | φ = A x | φ
4 3 ineq2i B x A | φ = B A x | φ
5 incom x A | φ B = B x A | φ
6 in12 A B x | φ = B A x | φ
7 4 5 6 3eqtr4i x A | φ B = A B x | φ
8 2 7 eqtr4i A x B | φ = x A | φ B