Theorem bj-ceqsalt

Description: Remove from ceqsalt dependency on ax-ext (and on df-cleq and df-v ). Note: this is not doable with ceqsralt (or ceqsralv ), which uses eleq1 , but the same dependence removal is possible for ceqsalg , ceqsal , ceqsalv , cgsexg , cgsex2g , cgsex4g , ceqsex , ceqsexv , ceqsex2 , ceqsex2v , ceqsex3v , ceqsex4v , ceqsex6v , ceqsex8v , gencbvex (after changing A = y to y = A ), gencbvex2 , gencbval , vtoclgft (it uses F/_ , whose justification nfcjust does not use ax-ext ) and several other vtocl* theorems (see for instance bj-vtoclg1f ). See also bj-ceqsaltv . (Contributed by BJ, 16-Jun-2019) (Proof modification is discouraged.)

	Ref	Expression
Assertion	bj-ceqsalt	|- ( ( F/ x ps /\ A. x ( x = A -> ( ph <-> ps ) ) /\ A e. V ) -> ( A. x ( x = A -> ph ) <-> ps ) )

Proof

Step	Hyp	Ref	Expression
1		elisset	|- ( A e. V -> E. x x = A )
2	1	3anim3i	|- ( ( F/ x ps /\ A. x ( x = A -> ( ph <-> ps ) ) /\ A e. V ) -> ( F/ x ps /\ A. x ( x = A -> ( ph <-> ps ) ) /\ E. x x = A ) )
3		bj-ceqsalt0	|- ( ( F/ x ps /\ A. x ( x = A -> ( ph <-> ps ) ) /\ E. x x = A ) -> ( A. x ( x = A -> ph ) <-> ps ) )
4	2 3	syl	|- ( ( F/ x ps /\ A. x ( x = A -> ( ph <-> ps ) ) /\ A e. V ) -> ( A. x ( x = A -> ph ) <-> ps ) )