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
|- F/ x ph
bj-cbv2v.2
|- F/ y ph
bj-cbv2v.3
|- ( ph -> F/ y ps )
bj-cbv2v.4
|- ( ph -> F/ x ch )
bj-cbv2v.5
|- ( ph -> ( x = y -> ( ps <-> ch ) ) )
Assertion bj-cbv2v
|- ( ph -> ( A. x ps <-> A. y ch ) )

Proof

Step Hyp Ref Expression
1 bj-cbv2v.1
 |-  F/ x ph
2 bj-cbv2v.2
 |-  F/ y ph
3 bj-cbv2v.3
 |-  ( ph -> F/ y ps )
4 bj-cbv2v.4
 |-  ( ph -> F/ x ch )
5 bj-cbv2v.5
 |-  ( ph -> ( x = y -> ( ps <-> ch ) ) )
6 2 nf5ri
 |-  ( ph -> A. y ph )
7 1 nfal
 |-  F/ x A. y ph
8 7 nf5ri
 |-  ( A. y ph -> A. x A. y ph )
9 6 8 syl
 |-  ( ph -> A. x A. y ph )
10 3 nf5rd
 |-  ( ph -> ( ps -> A. y ps ) )
11 4 nf5rd
 |-  ( ph -> ( ch -> A. x ch ) )
12 10 11 5 bj-cbv2hv
 |-  ( A. x A. y ph -> ( A. x ps <-> A. y ch ) )
13 9 12 syl
 |-  ( ph -> ( A. x ps <-> A. y ch ) )