Metamath Proof Explorer


Theorem bj-cbvexdv

Description: Version of cbvexd 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-cbvaldv.1 yφ
bj-cbvaldv.2 φyψ
bj-cbvaldv.3 φx=yψχ
Assertion bj-cbvexdv φxψyχ

Proof

Step Hyp Ref Expression
1 bj-cbvaldv.1 yφ
2 bj-cbvaldv.2 φyψ
3 bj-cbvaldv.3 φx=yψχ
4 2 nfnd φy¬ψ
5 notbi ψχ¬ψ¬χ
6 3 5 imbitrdi φx=y¬ψ¬χ
7 1 4 6 bj-cbvaldv φx¬ψy¬χ
8 7 notbid φ¬x¬ψ¬y¬χ
9 df-ex xψ¬x¬ψ
10 df-ex yχ¬y¬χ
11 8 9 10 3bitr4g φxψyχ