Theorem bj-ceqsalt 37254

Description: Remove from ceqsalt 3466 dependency on ax-ext 2713 (and on df-cleq 2733 and df-v 3435). Note: this is not doable with ceqsralt 3467 (or ceqsralv 3473), which uses eleq1 2829, but the same dependence removal is possible for ceqsalg 3468, ceqsal 3470, ceqsalv 3472, cgsexg 3477, cgsex2g 3478, cgsex4g 3479, ceqsex 3480, ceqsexv 3481, ceqsex2 3484, ceqsex2v 3485, ceqsex3v 3486, ceqsex4v 3487, ceqsex6v 3488, ceqsex8v 3489, gencbvex 3490 (after changing 𝐴 = 𝑦 to 𝑦 = 𝐴), gencbvex2 3491, gencbval 3492, vtoclgft 3500 (it uses Ⅎ, whose justification nfcjust 2889 does not use ax-ext 2713) and several other vtocl* theorems (see for instance bj-vtoclg1f 37286). See also bj-ceqsaltv 37255. (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 2823	. . 3 ⊢ (𝐴 ∈ 𝑉 → ∃𝑥 𝑥 = 𝐴)
2	1	3anim3i 1161	. 2 ⊢ ((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ 𝐴 ∈ 𝑉) → (Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ ∃𝑥 𝑥 = 𝐴))
3		bj-ceqsalt0 37252	. 2 ⊢ ((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ ∃𝑥 𝑥 = 𝐴) → (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓))
4	2, 3	syl 17	1 ⊢ ((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ 𝐴 ∈ 𝑉) → (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓))

Syntax hints:   → wi 4   ↔ wb 208   ∧ w3a 1093  ∀wal 1546   = wceq 1548  ∃wex 1787  Ⅎwnf 1791   ∈ wcel 2121

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-12 2191

This theorem depends on definitions:  df-bi 209  df-an 398  df-3an 1095  df-tru 1551  df-ex 1788  df-nf 1792  df-sb 2075  df-clab 2720  df-clel 2816

This theorem is referenced by:  bj-ceqsalgALT  37258