Metamath Proof Explorer


Theorem bj-cbval

Description: Changing a bound variable (universal quantification case) in a weak axiomatization, assuming that all variables denote (which is valid in inclusive free logic) and that equality is symmetric. (Contributed by BJ, 12-Mar-2023) (Proof modification is discouraged.)

Ref Expression
Hypotheses bj-cbval.denote
|- A. y E. x x = y
bj-cbval.denote2
|- A. x E. y y = x
bj-cbval.maj
|- ( x = y -> ( ph <-> ps ) )
bj-cbval.equcomiv
|- ( y = x -> x = y )
Assertion bj-cbval
|- ( A. x ph <-> A. y ps )

Proof

Step Hyp Ref Expression
1 bj-cbval.denote
 |-  A. y E. x x = y
2 bj-cbval.denote2
 |-  A. x E. y y = x
3 bj-cbval.maj
 |-  ( x = y -> ( ph <-> ps ) )
4 bj-cbval.equcomiv
 |-  ( y = x -> x = y )
5 3 biimpd
 |-  ( x = y -> ( ph -> ps ) )
6 5 1 bj-cbvalimi
 |-  ( A. x ph -> A. y ps )
7 3 biimprd
 |-  ( x = y -> ( ps -> ph ) )
8 4 7 syl
 |-  ( y = x -> ( ps -> ph ) )
9 8 2 bj-cbvalimi
 |-  ( A. y ps -> A. x ph )
10 6 9 impbii
 |-  ( A. x ph <-> A. y ps )