Theorem bj-ceqsalt 37376

Description: Remove from ceqsalt 3489 dependency on ax-ext 2736 (and on df-cleq 2756 and df-v 3458). Note: this is not doable with ceqsralt 3490 (or ceqsralv 3496), which uses eleq1 2852, but the same dependence removal is possible for ceqsalg 3491, ceqsal 3493, ceqsalv 3495, cgsexg 3500, cgsex2g 3501, cgsex4g 3502, ceqsex 3503, ceqsexv 3504, ceqsex2 3506, ceqsex2v 3507, ceqsex3v 3508, ceqsex4v 3509, ceqsex6v 3510, ceqsex8v 3511, gencbvex 3512 (after changing 𝐴 = 𝑦 to 𝑦 = 𝐴), gencbvex2 3513, gencbval 3514, vtoclgft 3522 (it uses Ⅎ, whose justification nfcjust 2912 does not use ax-ext 2736) and several other vtocl* theorems (see for instance bj-vtoclg1f 37408). See also bj-ceqsaltv 37377. (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 2846	. . 3 ⊢ (𝐴 ∈ 𝑉 → ∃𝑥 𝑥 = 𝐴)
2	1	3anim3i 1168	. 2 ⊢ ((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ 𝐴 ∈ 𝑉) → (Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ ∃𝑥 𝑥 = 𝐴))
3		bj-ceqsalt0 37374	. 2 ⊢ ((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ ∃𝑥 𝑥 = 𝐴) → (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓))
4	2, 3	syl 17	1 ⊢ ((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ 𝐴 ∈ 𝑉) → (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓))

Syntax hints:   → wi 4   ↔ wb 208   ∧ w3a 1099  ∀wal 1560   = wceq 1562  ∃wex 1801  Ⅎwnf 1805   ∈ wcel 2144

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-12 2214

This theorem depends on definitions:  df-bi 209  df-an 400  df-3an 1101  df-tru 1565  df-ex 1802  df-nf 1806  df-sb 2093  df-clab 2743  df-clel 2839

This theorem is referenced by:  bj-ceqsalgALT  37380