Theorem bj-ceqsalt 34998

Description: Remove from ceqsalt 3452 dependency on ax-ext 2709 (and on df-cleq 2730 and df-v 3424). Note: this is not doable with ceqsralt 3453 (or ceqsralv 3459), which uses eleq1 2826, but the same dependence removal is possible for ceqsalg 3454, ceqsal 3456, ceqsalv 3457, cgsexg 3464, cgsex2g 3465, cgsex4g 3466, ceqsex 3468, ceqsexv 3469, ceqsex2 3472, ceqsex2v 3473, ceqsex3v 3474, ceqsex4v 3475, ceqsex6v 3476, ceqsex8v 3477, gencbvex 3478 (after changing 𝐴 = 𝑦 to 𝑦 = 𝐴), gencbvex2 3479, gencbval 3480, vtoclgft 3482 (it uses Ⅎ, whose justification nfcjust 2887 does not use ax-ext 2709) and several other vtocl* theorems (see for instance bj-vtoclg1f 35030). See also bj-ceqsaltv 34999. (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 1152	. 2 ⊢ ((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ 𝐴 ∈ 𝑉) → (Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ ∃𝑥 𝑥 = 𝐴))
3		bj-ceqsalt0 34996	. 2 ⊢ ((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ ∃𝑥 𝑥 = 𝐴) → (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓))
4	2, 3	syl 17	1 ⊢ ((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ 𝐴 ∈ 𝑉) → (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓))

Syntax hints:   → wi 4   ↔ wb 205   ∧ w3a 1085  ∀wal 1537   = wceq 1539  ∃wex 1783  Ⅎwnf 1787   ∈ wcel 2108

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-12 2173

This theorem depends on definitions:  df-bi 206  df-an 396  df-3an 1087  df-tru 1542  df-ex 1784  df-nf 1788  df-sb 2069  df-clab 2716  df-clel 2817

This theorem is referenced by:  bj-ceqsalgALT  35002