Metamath Proof Explorer


Theorem rexeqbidvv

Description: Version of rexeqbidv with additional disjoint variable conditions, not requiring ax-8 nor df-clel . (Contributed by Wolf Lammen, 25-Sep-2024)

Ref Expression
Hypotheses raleqbidvv.1 φ A = B
raleqbidvv.2 φ ψ χ
Assertion rexeqbidvv φ 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 rexeqbidva φ x A ψ x B χ