Theorem bj-ceqsalt 36930

Description: Remove from ceqsalt 3470 dependency on ax-ext 2703 (and on df-cleq 2723 and df-v 3438). Note: this is not doable with ceqsralt 3471 (or ceqsralv 3477), which uses eleq1 2819, but the same dependence removal is possible for ceqsalg 3472, ceqsal 3474, ceqsalv 3476, cgsexg 3481, cgsex2g 3482, cgsex4g 3483, ceqsex 3485, ceqsexv 3486, ceqsex2 3489, ceqsex2v 3490, ceqsex3v 3491, ceqsex4v 3492, ceqsex6v 3493, ceqsex8v 3494, gencbvex 3495 (after changing 𝐴 = 𝑦 to 𝑦 = 𝐴), gencbvex2 3496, gencbval 3497, vtoclgft 3505 (it uses Ⅎ, whose justification nfcjust 2880 does not use ax-ext 2703) and several other vtocl* theorems (see for instance bj-vtoclg1f 36962). See also bj-ceqsaltv 36931. (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 2813	. . 3 ⊢ (𝐴 ∈ 𝑉 → ∃𝑥 𝑥 = 𝐴)
2	1	3anim3i 1154	. 2 ⊢ ((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ 𝐴 ∈ 𝑉) → (Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ ∃𝑥 𝑥 = 𝐴))
3		bj-ceqsalt0 36928	. 2 ⊢ ((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ ∃𝑥 𝑥 = 𝐴) → (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓))
4	2, 3	syl 17	1 ⊢ ((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ 𝐴 ∈ 𝑉) → (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓))

Syntax hints:   → wi 4   ↔ wb 206   ∧ w3a 1086  ∀wal 1539   = wceq 1541  ∃wex 1780  Ⅎwnf 1784   ∈ wcel 2111

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 1968  ax-7 2009  ax-8 2113  ax-12 2180

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1544  df-ex 1781  df-nf 1785  df-sb 2068  df-clab 2710  df-clel 2806

This theorem is referenced by:  bj-ceqsalgALT  36934