Metamath Proof Explorer


Theorem bj-inrab

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

Ref Expression
Assertion bj-inrab x A | φ x B | ψ = x A B | φ ψ

Proof

Step Hyp Ref Expression
1 an4 x A φ x B ψ x A x B φ ψ
2 elin x A B x A x B
3 2 anbi1i x A B φ ψ x A x B φ ψ
4 1 3 bitr4i x A φ x B ψ x A B φ ψ
5 4 abbii x | x A φ x B ψ = x | x A B φ ψ
6 df-rab x A | φ = x | x A φ
7 df-rab x B | ψ = x | x B ψ
8 6 7 ineq12i x A | φ x B | ψ = x | x A φ x | x B ψ
9 inab x | x A φ x | x B ψ = x | x A φ x B ψ
10 8 9 eqtri x A | φ x B | ψ = x | x A φ x B ψ
11 df-rab x A B | φ ψ = x | x A B φ ψ
12 5 10 11 3eqtr4i x A | φ x B | ψ = x A B | φ ψ