Theorem bj-ceqsalt 37720

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 37752). See also bj-ceqsaltv 37721. (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 37718	. 2 ⊢ ((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ ∃𝑥 𝑥 = 𝐴) → (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓))
4	2, 3	syl 18	1 ⊢ ((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ 𝐴 ∈ 𝑉) → (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ w3a 1103  ∀wal 1568   = wceq 1570  ∃wex 1812  Ⅎwnf 1816   ∈ wcel 2145

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-12 2213

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105  df-tru 1573  df-ex 1813  df-nf 1817  df-sb 2100  df-clab 2739  df-clel 2835

This theorem is used by:  bj-ceqsalgALT  37724