Theorem bj-ceqsalt 36862

Description: Remove from ceqsalt 3498 dependency on ax-ext 2706 (and on df-cleq 2726 and df-v 3465). Note: this is not doable with ceqsralt 3499 (or ceqsralv 3505), which uses eleq1 2821, but the same dependence removal is possible for ceqsalg 3500, ceqsal 3502, ceqsalv 3504, cgsexg 3509, cgsex2g 3510, cgsex4g 3511, ceqsex 3513, ceqsexv 3515, ceqsex2 3518, ceqsex2v 3519, ceqsex3v 3520, ceqsex4v 3521, ceqsex6v 3522, ceqsex8v 3523, gencbvex 3524 (after changing 𝐴 = 𝑦 to 𝑦 = 𝐴), gencbvex2 3525, gencbval 3526, vtoclgft 3535 (it uses Ⅎ, whose justification nfcjust 2883 does not use ax-ext 2706) and several other vtocl* theorems (see for instance bj-vtoclg1f 36894). See also bj-ceqsaltv 36863. (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		elisset 2815	. . 3 ⊢ (𝐴 ∈ 𝑉 → ∃𝑥 𝑥 = 𝐴)
2	1	3anim3i 1154	. 2 ⊢ ((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ 𝐴 ∈ 𝑉) → (Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ ∃𝑥 𝑥 = 𝐴))
3		bj-ceqsalt0 36860	. 2 ⊢ ((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ ∃𝑥 𝑥 = 𝐴) → (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓))
4	2, 3	syl 17	1 ⊢ ((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ 𝐴 ∈ 𝑉) → (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓))

Syntax hints:   → wi 4   ↔ wb 206   ∧ w3a 1086  ∀wal 1537   = wceq 1539  ∃wex 1778  Ⅎwnf 1782   ∈ wcel 2107

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-12 2176

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1542  df-ex 1779  df-nf 1783  df-sb 2064  df-clab 2713  df-clel 2808

This theorem is referenced by:  bj-ceqsalgALT  36866