Metamath Proof Explorer


Theorem cbvex2v

Description: Rule used to change bound variables, using implicit substitution. Version of cbvex2 with a disjoint variable condition, which does not require ax-13 . (Contributed by NM, 14-Sep-2003) (Revised by BJ, 16-Jun-2019)

Ref Expression
Hypotheses cbval2v.1 z φ
cbval2v.2 w φ
cbval2v.3 x ψ
cbval2v.4 y ψ
cbval2v.5 x = z y = w φ ψ
Assertion cbvex2v x y φ z w ψ

Proof

Step Hyp Ref Expression
1 cbval2v.1 z φ
2 cbval2v.2 w φ
3 cbval2v.3 x ψ
4 cbval2v.4 y ψ
5 cbval2v.5 x = z y = w φ ψ
6 1 nfn z ¬ φ
7 2 nfn w ¬ φ
8 3 nfn x ¬ ψ
9 4 nfn y ¬ ψ
10 5 notbid x = z y = w ¬ φ ¬ ψ
11 6 7 8 9 10 cbval2v x y ¬ φ z w ¬ ψ
12 2nexaln ¬ x y φ x y ¬ φ
13 2nexaln ¬ z w ψ z w ¬ ψ
14 11 12 13 3bitr4i ¬ x y φ ¬ z w ψ
15 14 con4bii x y φ z w ψ