Metamath Proof Explorer


Theorem raleqbidvv

Description: Version of raleqbidv with additional disjoint variable conditions, not requiring ax-8 nor df-clel . (Contributed by BJ, 22-Sep-2024)

Ref Expression
Hypotheses raleqbidvv.1 φ A = B
raleqbidvv.2 φ ψ χ
Assertion raleqbidvv φ x A ψ x B χ

Proof

Step Hyp Ref Expression
1 raleqbidvv.1 φ A = B
2 raleqbidvv.2 φ ψ χ
3 2 adantr φ x A ψ χ
4 1 3 raleqbidva φ x A ψ x B χ