Metamath Proof Explorer


Theorem bj-cbvex

Description: Changing a bound variable (existential 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-cbvex
|- ( E. x ph <-> E. 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 4 5 syl
 |-  ( y = x -> ( ph -> ps ) )
7 6 2 bj-cbveximi
 |-  ( E. x ph -> E. y ps )
8 3 biimprd
 |-  ( x = y -> ( ps -> ph ) )
9 8 1 bj-cbveximi
 |-  ( E. y ps -> E. x ph )
10 7 9 impbii
 |-  ( E. x ph <-> E. y ps )