Metamath Proof Explorer


Theorem cbv3v2

Description: Version of cbv3 with two disjoint variable conditions, which does not require ax-11 nor ax-13 . (Contributed by BJ, 24-Jun-2019) (Proof shortened by Wolf Lammen, 30-Aug-2021)

Ref Expression
Hypotheses cbv3v2.nf x ψ
cbv3v2.1 x = y φ ψ
Assertion cbv3v2 x φ y ψ

Proof

Step Hyp Ref Expression
1 cbv3v2.nf x ψ
2 cbv3v2.1 x = y φ ψ
3 1 2 spimfv x φ ψ
4 3 alrimiv x φ y ψ