Metamath Proof Explorer


Theorem bj-rabbida2

Description: Version of rabbidva2 with disjoint variable condition replaced by nonfreeness hypothesis. (Contributed by BJ, 27-Apr-2019)

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

Proof

Step Hyp Ref Expression
1 bj-rabbida2.nf x φ
2 bj-rabbida2.1 φ x A ψ x B χ
3 1 2 abbid φ x | x A ψ = x | x B χ
4 df-rab x A | ψ = x | x A ψ
5 df-rab x B | χ = x | x B χ
6 3 4 5 3eqtr4g φ x A | ψ = x B | χ