Theorem bj-ceqsalt 37469

Description: Remove from ceqsalt 3495 dependency on ax-ext 2742 (and on df-cleq 2762 and df-v 3464). Note: this is not doable with ceqsralt 3496 (or ceqsralv 3502), which uses eleq1 2858, but the same dependence removal is possible for ceqsalg 3497, ceqsal 3499, ceqsalv 3501, cgsexg 3506, cgsex2g 3507, cgsex4g 3508, ceqsex 3509, ceqsexv 3510, ceqsex2 3512, ceqsex2v 3513, ceqsex3v 3514, ceqsex4v 3515, ceqsex6v 3516, ceqsex8v 3517, gencbvex 3518 (after changing 𝐴 = 𝑦 to 𝑦 = 𝐴), gencbvex2 3519, gencbval 3520, vtoclgft 3528 (it uses Ⅎ, whose justification nfcjust 2918 does not use ax-ext 2742) and several other vtocl* theorems (see for instance bj-vtoclg1f 37501). See also bj-ceqsaltv 37470. (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 2852	. . 3 ⊢ (𝐴 ∈ 𝑉 → ∃𝑥 𝑥 = 𝐴)
2	1	3anim3i 1170	. 2 ⊢ ((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ 𝐴 ∈ 𝑉) → (Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ ∃𝑥 𝑥 = 𝐴))
3		bj-ceqsalt0 37467	. 2 ⊢ ((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ ∃𝑥 𝑥 = 𝐴) → (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓))
4	2, 3	syl 18	1 ⊢ ((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ 𝐴 ∈ 𝑉) → (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓))

Syntax hints:   → wi 4   ↔ wb 209   ∧ w3a 1101  ∀wal 1566   = wceq 1568  ∃wex 1807  Ⅎwnf 1811   ∈ wcel 2150

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-8 2152  ax-12 2220

This theorem depends on definitions:  df-bi 210  df-an 401  df-3an 1103  df-tru 1571  df-ex 1808  df-nf 1812  df-sb 2099  df-clab 2749  df-clel 2845

This theorem is referenced by:  bj-ceqsalgALT  37473