Theorem bj-ceqsalt 34204

Description: Remove from ceqsalt 3529 dependency on ax-ext 2795 (and on df-cleq 2816 and df-v 3498). Note: this is not doable with ceqsralt 3530 (or ceqsralv 3535), which uses eleq1 2902, but the same dependence removal is possible for ceqsalg 3531, ceqsal 3533, ceqsalv 3534, cgsexg 3539, cgsex2g 3540, cgsex4g 3541, ceqsex 3542, ceqsexv 3543, ceqsex2 3545, ceqsex2v 3546, ceqsex3v 3547, ceqsex4v 3548, ceqsex6v 3549, ceqsex8v 3550, gencbvex 3551 (after changing 𝐴 = 𝑦 to 𝑦 = 𝐴), gencbvex2 3552, gencbval 3553, vtoclgft 3555 (it uses Ⅎ, whose justification nfcjust 2964 does not use ax-ext 2795) and several other vtocl* theorems (see for instance bj-vtoclg1f 34236). See also bj-ceqsaltv 34205. (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 34194	. . 3 ⊢ (𝐴 ∈ 𝑉 → ∃𝑥 𝑥 = 𝐴)
2	1	3anim3i 1150	. 2 ⊢ ((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ 𝐴 ∈ 𝑉) → (Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ ∃𝑥 𝑥 = 𝐴))
3		bj-ceqsalt0 34202	. 2 ⊢ ((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ ∃𝑥 𝑥 = 𝐴) → (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓))
4	2, 3	syl 17	1 ⊢ ((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ 𝐴 ∈ 𝑉) → (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓))

Syntax hints:   → wi 4   ↔ wb 208   ∧ w3a 1083  ∀wal 1535   = wceq 1537  ∃wex 1780  Ⅎwnf 1784   ∈ wcel 2114

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-12 2177

This theorem depends on definitions:  df-bi 209  df-an 399  df-3an 1085  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-clel 2895

This theorem is referenced by:  bj-ceqsalgALT  34208