Metamath Proof Explorer


Theorem bj-rabeqbid

Description: Version of rabeqbidv with two disjoint variable conditions removed and the third replaced by a nonfreeness hypothesis. (Contributed by BJ, 27-Apr-2019)

Ref Expression
Hypotheses bj-rabeqbid.nf x φ
bj-rabeqbid.1 φ A = B
bj-rabeqbid.2 φ ψ χ
Assertion bj-rabeqbid φ x A | ψ = x B | χ

Proof

Step Hyp Ref Expression
1 bj-rabeqbid.nf x φ
2 bj-rabeqbid.1 φ A = B
3 bj-rabeqbid.2 φ ψ χ
4 1 2 bj-rabeqd φ x A | ψ = x B | ψ
5 1 3 rabbid φ x B | ψ = x B | χ
6 4 5 eqtrd φ x A | ψ = x B | χ