Theorem bj-ceqsalt 35071

Description: Remove from ceqsalt 3462 dependency on ax-ext 2709 (and on df-cleq 2730 and df-v 3434). Note: this is not doable with ceqsralt 3463 (or ceqsralv 3469), which uses eleq1 2826, but the same dependence removal is possible for ceqsalg 3464, ceqsal 3466, ceqsalv 3467, cgsexg 3474, cgsex2g 3475, cgsex4g 3476, ceqsex 3478, ceqsexv 3479, ceqsex2 3482, ceqsex2v 3483, ceqsex3v 3484, ceqsex4v 3485, ceqsex6v 3486, ceqsex8v 3487, gencbvex 3488 (after changing 𝐴 = 𝑦 to 𝑦 = 𝐴), gencbvex2 3489, gencbval 3490, vtoclgft 3492 (it uses Ⅎ, whose justification nfcjust 2888 does not use ax-ext 2709) and several other vtocl* theorems (see for instance bj-vtoclg1f 35103). See also bj-ceqsaltv 35072. (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 2820	. . 3 ⊢ (𝐴 ∈ 𝑉 → ∃𝑥 𝑥 = 𝐴)
2	1	3anim3i 1153	. 2 ⊢ ((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ 𝐴 ∈ 𝑉) → (Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ ∃𝑥 𝑥 = 𝐴))
3		bj-ceqsalt0 35069	. 2 ⊢ ((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ ∃𝑥 𝑥 = 𝐴) → (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓))
4	2, 3	syl 17	1 ⊢ ((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ 𝐴 ∈ 𝑉) → (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓))

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-12 2171

This theorem depends on definitions:  df-bi 206  df-an 397  df-3an 1088  df-tru 1542  df-ex 1783  df-nf 1787  df-sb 2068  df-clab 2716  df-clel 2816

This theorem is referenced by:  bj-ceqsalgALT  35075