Theorem bj-ceqsalt 37798

Description: Remove from ceqsalt 3483 dependency on ax-ext 2732 (and on df-cleq 2752 and df-v 3452). Note: this is not doable with ceqsralt 3484 (or ceqsralv 3490), which uses eleq1 2848, but the same dependence removal is possible for ceqsalg 3485, ceqsal 3487, ceqsalv 3489, cgsexg 3494, cgsex2g 3495, cgsex4g 3496, ceqsex 3497, ceqsexv 3498, ceqsex2 3500, ceqsex2v 3501, ceqsex3v 3502, ceqsex4v 3503, ceqsex6v 3504, ceqsex8v 3505, gencbvex 3506 (after changing 𝐴 = 𝑦 to 𝑦 = 𝐴), gencbvex2 3507, gencbval 3508, vtoclgft 3515 (it uses Ⅎ, whose justification nfcjust 2908 does not use ax-ext 2732) and several other vtocl* theorems (see for instance bj-vtoclg1f 37830). See also bj-ceqsaltv 37799. (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 2842	. . 3 ⊢ (𝐴 ∈ 𝑉 → ∃𝑥 𝑥 = 𝐴)
2	1	3anim3i 1172	. 2 ⊢ ((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ 𝐴 ∈ 𝑉) → (Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ ∃𝑥 𝑥 = 𝐴))
3		bj-ceqsalt0 37796	. 2 ⊢ ((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ ∃𝑥 𝑥 = 𝐴) → (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓))
4	2, 3	syl 18	1 ⊢ ((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ 𝐴 ∈ 𝑉) → (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ w3a 1103  ∀wal 1567   = wceq 1569  ∃wex 1811  Ⅎwnf 1815   ∈ wcel 2144

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-12 2212

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105  df-tru 1572  df-ex 1812  df-nf 1816  df-sb 2099  df-clab 2739  df-clel 2835

This theorem is used by:  bj-ceqsalgALT  37802