Metamath Proof Explorer


Theorem bj-cbv2v

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

Ref Expression
Hypotheses bj-cbv2v.1 x φ
bj-cbv2v.2 y φ
bj-cbv2v.3 φ y ψ
bj-cbv2v.4 φ x χ
bj-cbv2v.5 φ x = y ψ χ
Assertion bj-cbv2v φ x ψ y χ

Proof

Step Hyp Ref Expression
1 bj-cbv2v.1 x φ
2 bj-cbv2v.2 y φ
3 bj-cbv2v.3 φ y ψ
4 bj-cbv2v.4 φ x χ
5 bj-cbv2v.5 φ x = y ψ χ
6 2 nf5ri φ y φ
7 1 nfal x y φ
8 7 nf5ri y φ x y φ
9 6 8 syl φ x y φ
10 3 nf5rd φ ψ y ψ
11 4 nf5rd φ χ x χ
12 10 11 5 bj-cbv2hv x y φ x ψ y χ
13 9 12 syl φ x ψ y χ