Theorem bj-ceqsalt 32069

Description: Remove from ceqsalt 3201 dependency on ax-ext 2590 (and on df-cleq 2603 and df-v 3175). Note: this is not doable with ceqsralt 3202 (or ceqsralv 3207), which uses eleq1 2676, but the same dependence removal is possible for ceqsalg 3203, ceqsal 3205, ceqsalv 3206, cgsexg 3211, cgsex2g 3212, cgsex4g 3213, ceqsex 3214, ceqsexv 3215, ceqsex2 3217, ceqsex2v 3218, ceqsex3v 3219, ceqsex4v 3220, ceqsex6v 3221, ceqsex8v 3222, gencbvex 3223 (after changing 𝐴 = 𝑦 to 𝑦 = 𝐴), gencbvex2 3224, gencbval 3225, vtoclgft 3227 (it uses Ⅎ, whose justification nfcjust 2739 is actually provable without ax-ext 2590, as bj-nfcjust 32044 shows) and several other vtocl* theorems (see for instance bj-vtoclg1f 32103). See also bj-ceqsaltv 32070. (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 32056	. . 3 ⊢ (𝐴 ∈ 𝑉 → ∃𝑥 𝑥 = 𝐴)
2	1	3anim3i 1243	. 2 ⊢ ((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ 𝐴 ∈ 𝑉) → (Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ ∃𝑥 𝑥 = 𝐴))
3		bj-ceqsalt0 32067	. 2 ⊢ ((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ ∃𝑥 𝑥 = 𝐴) → (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓))
4	2, 3	syl 17	1 ⊢ ((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ 𝐴 ∈ 𝑉) → (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓))

Syntax hints:   → wi 4   ↔ wb 195   ∧ w3a 1031  ∀wal 1473   = wceq 1475  ∃wex 1695  Ⅎwnf 1699   ∈ wcel 1977

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-12 2034

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-clel 2606

This theorem is referenced by:  bj-ceqsalgALT  32073