Metamath Proof Explorer


Theorem bj-rabeqbida

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

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

Proof

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