Theorem bj-ceqsalt 34637

Description: Remove from ceqsalt 3132 dependency on ax-ext 2435 (and on df-cleq 2449 and df-v 3111). Note: this is not doable with ceqsralt 3133 (or ceqsralv 3138), which uses eleq1 2529, but the same dependence removal is possible for ceqsalg 3134, ceqsal 3136, ceqsalv 3137, cgsexg 3142, cgsex2g 3143, cgsex4g 3144, ceqsex 3145, ceqsexv 3146, ceqsex2 3147, ceqsex2v 3148, ceqsex3v 3149, ceqsex4v 3150, ceqsex6v 3151, ceqsex8v 3152, gencbvex 3153 (after changing A = y to y = A), gencbvex2 3154, gencbval 3155, vtoclgft 3157 (it uses F/_, whose justification nfcjust 2606 is actually provable without ax-ext 2435, as bj-nfcjust 34612 shows) and several other vtocl* theorems (see for instance bj-vtoclg1f 34669). See also bj-ceqsaltv 34638. (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 34624	. . 3 |- ( A e. V -> E. x x = A )
2	1	3anim3i 1184	. 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 34635	. 2 |- ( ( F/ x ps /\ A. x ( x = A -> ( ph <-> ps ) ) /\ E. x x = A ) -> ( A. x ( x = A -> ph ) <-> ps ) )
4	2, 3	syl 16	1 |- ( ( F/ x ps /\ A. x ( x = A -> ( ph <-> ps ) ) /\ A e. V ) -> ( A. x ( x = A -> ph ) <-> ps ) )

Syntax hints:   -> wi 4   <-> wb 184   /\ w3a 973   A.wal 1393   = wceq 1395   E.wex 1613   F/wnf 1617   e. wcel 1819

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-10 1838  ax-12 1855

This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 975  df-ex 1614  df-nf 1618  df-sb 1741  df-clab 2443  df-clel 2452

This theorem is referenced by:  bj-ceqsalgALT  34641