Theorem bj-ceqsalt 35766

Description: Remove from ceqsalt 3506 dependency on ax-ext 2704 (and on df-cleq 2725 and df-v 3477). Note: this is not doable with ceqsralt 3507 (or ceqsralv 3514), which uses eleq1 2822, but the same dependence removal is possible for ceqsalg 3508, ceqsal 3510, ceqsalv 3512, cgsexg 3519, cgsex2g 3520, cgsex4g 3521, ceqsex 3524, ceqsexv 3526, ceqsex2 3530, ceqsex2v 3531, ceqsex3v 3532, ceqsex4v 3533, ceqsex6v 3534, ceqsex8v 3535, gencbvex 3536 (after changing 𝐴 = 𝑦 to 𝑦 = 𝐴), gencbvex2 3537, gencbval 3538, vtoclgft 3541 (it uses Ⅎ, whose justification nfcjust 2885 does not use ax-ext 2704) and several other vtocl* theorems (see for instance bj-vtoclg1f 35798). See also bj-ceqsaltv 35767. (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 2816	. . 3 ⊢ (𝐴 ∈ 𝑉 → ∃𝑥 𝑥 = 𝐴)
2	1	3anim3i 1155	. 2 ⊢ ((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ 𝐴 ∈ 𝑉) → (Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ ∃𝑥 𝑥 = 𝐴))
3		bj-ceqsalt0 35764	. 2 ⊢ ((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ ∃𝑥 𝑥 = 𝐴) → (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓))
4	2, 3	syl 17	1 ⊢ ((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ 𝐴 ∈ 𝑉) → (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓))

Syntax hints:   → wi 4   ↔ wb 205   ∧ w3a 1088  ∀wal 1540   = wceq 1542  ∃wex 1782  Ⅎwnf 1786   ∈ wcel 2107

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-12 2172

This theorem depends on definitions:  df-bi 206  df-an 398  df-3an 1090  df-tru 1545  df-ex 1783  df-nf 1787  df-sb 2069  df-clab 2711  df-clel 2811

This theorem is referenced by:  bj-ceqsalgALT  35770