Theorem bj-ceqsalt 32875

Description: Remove from ceqsalt 3228 dependency on ax-ext 2602 (and on df-cleq 2615 and df-v 3202). Note: this is not doable with ceqsralt 3229 (or ceqsralv 3234), which uses eleq1 2689, but the same dependence removal is possible for ceqsalg 3230, ceqsal 3232, ceqsalv 3233, cgsexg 3238, cgsex2g 3239, cgsex4g 3240, ceqsex 3241, ceqsexv 3242, ceqsex2 3244, ceqsex2v 3245, ceqsex3v 3246, ceqsex4v 3247, ceqsex6v 3248, ceqsex8v 3249, gencbvex 3250 (after changing 𝐴 = 𝑦 to 𝑦 = 𝐴), gencbvex2 3251, gencbval 3252, vtoclgft 3254 (it uses Ⅎ, whose justification nfcjust 2752 is actually provable without ax-ext 2602, as bj-nfcjust 32850 shows) and several other vtocl* theorems (see for instance bj-vtoclg1f 32911). See also bj-ceqsaltv 32876. (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.)

Assertion

Ref	Expression
bj-ceqsalt	⊢ ((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ 𝐴 ∈ 𝑉) → (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓))

Distinct variable group:   𝑥,𝐴

Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑥)   𝑉(𝑥)

Proof of Theorem bj-ceqsalt

Step	Hyp	Ref	Expression
1		bj-elisset 32862	. . 3 ⊢ (𝐴 ∈ 𝑉 → ∃𝑥 𝑥 = 𝐴)
2	1	3anim3i 1250	. 2 ⊢ ((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ 𝐴 ∈ 𝑉) → (Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ ∃𝑥 𝑥 = 𝐴))
3		bj-ceqsalt0 32873	. 2 ⊢ ((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ ∃𝑥 𝑥 = 𝐴) → (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓))
4	2, 3	syl 17	1 ⊢ ((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ 𝐴 ∈ 𝑉) → (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓))

Syntax hints:   → wi 4   ↔ wb 196   ∧ w3a 1037  ∀wal 1481   = wceq 1483  ∃wex 1704  Ⅎwnf 1708   ∈ wcel 1990

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-12 2047

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-clel 2618

This theorem is referenced by:  bj-ceqsalgALT  32879