Theorem bj-ceqsalt 37181

Description: Remove from ceqsalt 3461 dependency on ax-ext 2707 (and on df-cleq 2727 and df-v 3429). Note: this is not doable with ceqsralt 3462 (or ceqsralv 3468), which uses eleq1 2823, but the same dependence removal is possible for ceqsalg 3463, ceqsal 3465, ceqsalv 3467, cgsexg 3472, cgsex2g 3473, cgsex4g 3474, ceqsex 3475, ceqsexv 3476, ceqsex2 3479, ceqsex2v 3480, ceqsex3v 3481, ceqsex4v 3482, ceqsex6v 3483, ceqsex8v 3484, gencbvex 3485 (after changing 𝐴 = 𝑦 to 𝑦 = 𝐴), gencbvex2 3486, gencbval 3487, vtoclgft 3495 (it uses Ⅎ, whose justification nfcjust 2883 does not use ax-ext 2707) and several other vtocl* theorems (see for instance bj-vtoclg1f 37213). See also bj-ceqsaltv 37182. (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 2817	. . 3 ⊢ (𝐴 ∈ 𝑉 → ∃𝑥 𝑥 = 𝐴)
2	1	3anim3i 1155	. 2 ⊢ ((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ 𝐴 ∈ 𝑉) → (Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ ∃𝑥 𝑥 = 𝐴))
3		bj-ceqsalt0 37179	. 2 ⊢ ((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ ∃𝑥 𝑥 = 𝐴) → (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓))
4	2, 3	syl 17	1 ⊢ ((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ 𝐴 ∈ 𝑉) → (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓))

Syntax hints:   → wi 4   ↔ wb 206   ∧ w3a 1087  ∀wal 1540   = wceq 1542  ∃wex 1781  Ⅎwnf 1785   ∈ wcel 2114

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-12 2184

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1089  df-tru 1545  df-ex 1782  df-nf 1786  df-sb 2069  df-clab 2714  df-clel 2810

This theorem is referenced by:  bj-ceqsalgALT  37185