Theorem bj-ceqsalt 37060

Description: Remove from ceqsalt 3473 dependency on ax-ext 2707 (and on df-cleq 2727 and df-v 3441). Note: this is not doable with ceqsralt 3474 (or ceqsralv 3480), which uses eleq1 2823, but the same dependence removal is possible for ceqsalg 3475, ceqsal 3477, ceqsalv 3479, cgsexg 3484, cgsex2g 3485, cgsex4g 3486, ceqsex 3488, ceqsexv 3489, ceqsex2 3492, ceqsex2v 3493, ceqsex3v 3494, ceqsex4v 3495, ceqsex6v 3496, ceqsex8v 3497, gencbvex 3498 (after changing 𝐴 = 𝑦 to 𝑦 = 𝐴), gencbvex2 3499, gencbval 3500, vtoclgft 3508 (it uses Ⅎ, whose justification nfcjust 2883 does not use ax-ext 2707) and several other vtocl* theorems (see for instance bj-vtoclg1f 37092). See also bj-ceqsaltv 37061. (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 2817	. . 3 ⊢ (𝐴 ∈ 𝑉 → ∃𝑥 𝑥 = 𝐴)
2	1	3anim3i 1155	. 2 ⊢ ((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ 𝐴 ∈ 𝑉) → (Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ ∃𝑥 𝑥 = 𝐴))
3		bj-ceqsalt0 37058	. 2 ⊢ ((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ ∃𝑥 𝑥 = 𝐴) → (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓))
4	2, 3	syl 17	1 ⊢ ((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ 𝐴 ∈ 𝑉) → (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓))

Syntax hints:   → wi 4   ↔ wb 206   ∧ w3a 1087  ∀wal 1540   = wceq 1542  ∃wex 1781  Ⅎwnf 1785   ∈ wcel 2114

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-12 2183

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1089  df-tru 1545  df-ex 1782  df-nf 1786  df-sb 2069  df-clab 2714  df-clel 2810

This theorem is referenced by:  bj-ceqsalgALT  37064