Theorem bj-equsexval

Description: Special case of equsexv proved from core axioms, ax-10 (modal5), and hba1 (modal4). (Contributed by BJ, 29-Dec-2020) (Proof modification is discouraged.)

	Ref	Expression
Hypothesis	bj-equsexval.1	|- ( x = y -> ( ph <-> A. x ps ) )
Assertion	bj-equsexval	|- ( E. x ( x = y /\ ph ) <-> A. x ps )

Proof

Step	Hyp	Ref	Expression
1		bj-equsexval.1	|- ( x = y -> ( ph <-> A. x ps ) )
2	1	pm5.32i	|- ( ( x = y /\ ph ) <-> ( x = y /\ A. x ps ) )
3	2	exbii	|- ( E. x ( x = y /\ ph ) <-> E. x ( x = y /\ A. x ps ) )
4		ax6ev	|- E. x x = y
5		bj-19.41al	|- ( E. x ( x = y /\ A. x ps ) <-> ( E. x x = y /\ A. x ps ) )
6	4 5	mpbiran	|- ( E. x ( x = y /\ A. x ps ) <-> A. x ps )
7	3 6	bitri	|- ( E. x ( x = y /\ ph ) <-> A. x ps )