Metamath Proof Explorer


Theorem bj-cbv3hv2

Description: Version of cbv3h with two disjoint variable conditions, which does not require ax-11 nor ax-13 . (Contributed by BJ, 24-Jun-2019) (Proof modification is discouraged.)

Ref Expression
Hypotheses bj-cbv3hv2.nf
|- ( ps -> A. x ps )
bj-cbv3hv2.1
|- ( x = y -> ( ph -> ps ) )
Assertion bj-cbv3hv2
|- ( A. x ph -> A. y ps )

Proof

Step Hyp Ref Expression
1 bj-cbv3hv2.nf
 |-  ( ps -> A. x ps )
2 bj-cbv3hv2.1
 |-  ( x = y -> ( ph -> ps ) )
3 1 nf5i
 |-  F/ x ps
4 3 2 cbv3v2
 |-  ( A. x ph -> A. y ps )