Theorem bj-ceqsalt 36829

Description: Remove from ceqsalt 3512 dependency on ax-ext 2704 (and on df-cleq 2725 and df-v 3479). Note: this is not doable with ceqsralt 3513 (or ceqsralv 3519), which uses eleq1 2825, but the same dependence removal is possible for ceqsalg 3514, ceqsal 3516, ceqsalv 3518, cgsexg 3523, cgsex2g 3524, cgsex4g 3525, ceqsex 3527, ceqsexv 3529, ceqsex2 3534, ceqsex2v 3535, ceqsex3v 3536, ceqsex4v 3537, ceqsex6v 3538, ceqsex8v 3539, gencbvex 3540 (after changing 𝐴 = 𝑦 to 𝑦 = 𝐴), gencbvex2 3541, gencbval 3542, vtoclgft 3551 (it uses Ⅎ, whose justification nfcjust 2887 does not use ax-ext 2704) and several other vtocl* theorems (see for instance bj-vtoclg1f 36861). See also bj-ceqsaltv 36830. (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 2819	. . 3 ⊢ (𝐴 ∈ 𝑉 → ∃𝑥 𝑥 = 𝐴)
2	1	3anim3i 1152	. 2 ⊢ ((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ 𝐴 ∈ 𝑉) → (Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ ∃𝑥 𝑥 = 𝐴))
3		bj-ceqsalt0 36827	. 2 ⊢ ((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ ∃𝑥 𝑥 = 𝐴) → (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓))
4	2, 3	syl 17	1 ⊢ ((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ 𝐴 ∈ 𝑉) → (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓))

Syntax hints:   → wi 4   ↔ wb 206   ∧ w3a 1085  ∀wal 1533   = wceq 1535  ∃wex 1774  Ⅎwnf 1778   ∈ wcel 2104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1963  ax-7 2003  ax-8 2106  ax-12 2173

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1087  df-tru 1538  df-ex 1775  df-nf 1779  df-sb 2061  df-clab 2711  df-clel 2812

This theorem is referenced by:  bj-ceqsalgALT  36833