Theorem bj-ceqsalt 35634

Description: Remove from ceqsalt 3504 dependency on ax-ext 2703 (and on df-cleq 2724 and df-v 3476). Note: this is not doable with ceqsralt 3505 (or ceqsralv 3512), which uses eleq1 2821, but the same dependence removal is possible for ceqsalg 3506, ceqsal 3508, ceqsalv 3510, cgsexg 3517, cgsex2g 3518, cgsex4g 3519, ceqsex 3521, ceqsexv 3523, ceqsex2 3527, ceqsex2v 3528, ceqsex3v 3529, ceqsex4v 3530, ceqsex6v 3531, ceqsex8v 3532, gencbvex 3533 (after changing 𝐴 = 𝑦 to 𝑦 = 𝐴), gencbvex2 3534, gencbval 3535, vtoclgft 3538 (it uses Ⅎ, whose justification nfcjust 2884 does not use ax-ext 2703) and several other vtocl* theorems (see for instance bj-vtoclg1f 35666). See also bj-ceqsaltv 35635. (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 35632	. 2 ⊢ ((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ ∃𝑥 𝑥 = 𝐴) → (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓))
4	2, 3	syl 17	1 ⊢ ((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ 𝐴 ∈ 𝑉) → (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓))

Syntax hints:   → wi 4   ↔ wb 205   ∧ w3a 1087  ∀wal 1539   = wceq 1541  ∃wex 1781  Ⅎwnf 1785   ∈ wcel 2106

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 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 1089  df-tru 1544  df-ex 1782  df-nf 1786  df-sb 2068  df-clab 2710  df-clel 2810

This theorem is referenced by:  bj-ceqsalgALT  35638