Theorem bj-ceqsalt 31496

Description: Remove from ceqsalt 3072 dependency on ax-ext 2433 (and on df-cleq 2446 and df-v 3049). Note: this is not doable with ceqsralt 3073 (or ceqsralv 3078), which uses eleq1 2519, but the same dependence removal is possible for ceqsalg 3074, ceqsal 3076, ceqsalv 3077, cgsexg 3082, cgsex2g 3083, cgsex4g 3084, ceqsex 3085, ceqsexv 3086, ceqsex2 3088, ceqsex2v 3089, ceqsex3v 3090, ceqsex4v 3091, ceqsex6v 3092, ceqsex8v 3093, gencbvex 3094 (after changing A = y to y = A), gencbvex2 3095, gencbval 3096, vtoclgft 3098 (it uses F/_, whose justification nfcjust 2582 is actually provable without ax-ext 2433, as bj-nfcjust 31471 shows) and several other vtocl* theorems (see for instance bj-vtoclg1f 31530). See also bj-ceqsaltv 31497. (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.)

Assertion

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

Distinct variable group:   x, A

Allowed substitution hints:   ph( x)   ps( x)   V( x)

Proof of Theorem bj-ceqsalt

Step	Hyp	Ref	Expression
1		bj-elisset 31483	. . 3 |- ( A e. V -> E. x x = A )
2	1	3anim3i 1197	. 2 |- ( ( 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 31494	. 2 |- ( ( F/ x ps /\ A. x ( x = A -> ( ph <-> ps ) ) /\ E. x x = A ) -> ( A. x ( x = A -> ph ) <-> ps ) )
4	2, 3	syl 17	1 |- ( ( F/ x ps /\ A. x ( x = A -> ( ph <-> ps ) ) /\ A e. V ) -> ( A. x ( x = A -> ph ) <-> ps ) )

Syntax hints:   -> wi 4   <-> wb 188   /\ w3a 986   A.wal 1444   = wceq 1446   E.wex 1665   F/wnf 1669   e. wcel 1889

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1671  ax-4 1684  ax-5 1760  ax-6 1807  ax-7 1853  ax-10 1917  ax-12 1935

This theorem depends on definitions:  df-bi 189  df-an 373  df-3an 988  df-ex 1666  df-nf 1670  df-sb 1800  df-clab 2440  df-clel 2449

This theorem is referenced by:  bj-ceqsalgALT  31500