Theorem bj-ceqsalt 36869

Description: Remove from ceqsalt 3484 dependency on ax-ext 2702 (and on df-cleq 2722 and df-v 3452). Note: this is not doable with ceqsralt 3485 (or ceqsralv 3491), which uses eleq1 2817, but the same dependence removal is possible for ceqsalg 3486, ceqsal 3488, ceqsalv 3490, cgsexg 3495, cgsex2g 3496, cgsex4g 3497, ceqsex 3499, ceqsexv 3501, ceqsex2 3504, ceqsex2v 3505, ceqsex3v 3506, ceqsex4v 3507, ceqsex6v 3508, ceqsex8v 3509, gencbvex 3510 (after changing 𝐴 = 𝑦 to 𝑦 = 𝐴), gencbvex2 3511, gencbval 3512, vtoclgft 3521 (it uses Ⅎ, whose justification nfcjust 2878 does not use ax-ext 2702) and several other vtocl* theorems (see for instance bj-vtoclg1f 36901). See also bj-ceqsaltv 36870. (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 2811	. . 3 ⊢ (𝐴 ∈ 𝑉 → ∃𝑥 𝑥 = 𝐴)
2	1	3anim3i 1154	. 2 ⊢ ((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ 𝐴 ∈ 𝑉) → (Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ ∃𝑥 𝑥 = 𝐴))
3		bj-ceqsalt0 36867	. 2 ⊢ ((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ ∃𝑥 𝑥 = 𝐴) → (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓))
4	2, 3	syl 17	1 ⊢ ((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ 𝐴 ∈ 𝑉) → (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓))

Syntax hints:   → wi 4   ↔ wb 206   ∧ w3a 1086  ∀wal 1538   = wceq 1540  ∃wex 1779  Ⅎwnf 1783   ∈ wcel 2109

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-12 2178

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1543  df-ex 1780  df-nf 1784  df-sb 2066  df-clab 2709  df-clel 2804

This theorem is referenced by:  bj-ceqsalgALT  36873