Metamath Proof Explorer


Theorem bj-cbvaldvav

Description: Version of cbvaldva with a disjoint variable condition, which does not require ax-13 . (Contributed by BJ, 16-Jun-2019) (Proof modification is discouraged.)

Ref Expression
Hypothesis bj-cbvaldvav.1 φ x = y ψ χ
Assertion bj-cbvaldvav φ x ψ y χ

Proof

Step Hyp Ref Expression
1 bj-cbvaldvav.1 φ x = y ψ χ
2 nfv y φ
3 nfvd φ y ψ
4 1 ex φ x = y ψ χ
5 2 3 4 bj-cbvaldv φ x ψ y χ