Theorem bj-ceqsalt 37549

Description: Remove from ceqsalt 3487 dependency on ax-ext 2734 (and on df-cleq 2754 and df-v 3456). Note: this is not doable with ceqsralt 3488 (or ceqsralv 3494), which uses eleq1 2850, but the same dependence removal is possible for ceqsalg 3489, ceqsal 3491, ceqsalv 3493, cgsexg 3498, cgsex2g 3499, cgsex4g 3500, ceqsex 3501, ceqsexv 3502, ceqsex2 3504, ceqsex2v 3505, ceqsex3v 3506, ceqsex4v 3507, ceqsex6v 3508, ceqsex8v 3509, gencbvex 3510 (after changing 𝐴 = 𝑦 to 𝑦 = 𝐴), gencbvex2 3511, gencbval 3512, vtoclgft 3519 (it uses Ⅎ, whose justification nfcjust 2910 does not use ax-ext 2734) and several other vtocl* theorems (see for instance bj-vtoclg1f 37581). See also bj-ceqsaltv 37550. (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 2844	. . 3 ⊢ (𝐴 ∈ 𝑉 → ∃𝑥 𝑥 = 𝐴)
2	1	3anim3i 1171	. 2 ⊢ ((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ 𝐴 ∈ 𝑉) → (Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ ∃𝑥 𝑥 = 𝐴))
3		bj-ceqsalt0 37547	. 2 ⊢ ((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ ∃𝑥 𝑥 = 𝐴) → (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓))
4	2, 3	syl 18	1 ⊢ ((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ 𝐴 ∈ 𝑉) → (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ w3a 1102  ∀wal 1567   = wceq 1569  ∃wex 1808  Ⅎwnf 1812   ∈ wcel 2142

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-12 2212

This proof depends on definitions:  df-bi 210  df-an 401  df-3an 1104  df-tru 1572  df-ex 1809  df-nf 1813  df-sb 2096  df-clab 2741  df-clel 2837

This theorem is used by:  bj-ceqsalgALT  37553