Theorem bj-ceqsalt 34808

Description: Remove from ceqsalt 3438 dependency on ax-ext 2708 (and on df-cleq 2729 and df-v 3410). Note: this is not doable with ceqsralt 3439 (or ceqsralv 3445), which uses eleq1 2825, but the same dependence removal is possible for ceqsalg 3440, ceqsal 3442, ceqsalv 3443, cgsexg 3450, cgsex2g 3451, cgsex4g 3452, ceqsex 3454, ceqsexv 3455, ceqsex2 3458, ceqsex2v 3459, ceqsex3v 3460, ceqsex4v 3461, ceqsex6v 3462, ceqsex8v 3463, gencbvex 3464 (after changing 𝐴 = 𝑦 to 𝑦 = 𝐴), gencbvex2 3465, gencbval 3466, vtoclgft 3468 (it uses Ⅎ, whose justification nfcjust 2885 does not use ax-ext 2708) and several other vtocl* theorems (see for instance bj-vtoclg1f 34840). See also bj-ceqsaltv 34809. (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		bj-elisset 34798	. . 3 ⊢ (𝐴 ∈ 𝑉 → ∃𝑥 𝑥 = 𝐴)
2	1	3anim3i 1156	. 2 ⊢ ((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ 𝐴 ∈ 𝑉) → (Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ ∃𝑥 𝑥 = 𝐴))
3		bj-ceqsalt0 34806	. 2 ⊢ ((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ ∃𝑥 𝑥 = 𝐴) → (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓))
4	2, 3	syl 17	1 ⊢ ((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ 𝐴 ∈ 𝑉) → (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓))

Syntax hints:   → wi 4   ↔ wb 209   ∧ w3a 1089  ∀wal 1541   = wceq 1543  ∃wex 1787  Ⅎwnf 1791   ∈ wcel 2110

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-12 2175

This theorem depends on definitions:  df-bi 210  df-an 400  df-3an 1091  df-tru 1546  df-ex 1788  df-nf 1792  df-sb 2071  df-clab 2715  df-clel 2816

This theorem is referenced by:  bj-ceqsalgALT  34812