Mathbox for BJ < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  bj-ceqsalt Structured version   Visualization version   GIF version

Theorem bj-ceqsalt 34477
 Description: Remove from ceqsalt 3475 dependency on ax-ext 2770 (and on df-cleq 2791 and df-v 3444). Note: this is not doable with ceqsralt 3476 (or ceqsralv 3481), which uses eleq1 2877, but the same dependence removal is possible for ceqsalg 3477, ceqsal 3479, ceqsalv 3480, cgsexg 3485, cgsex2g 3486, cgsex4g 3487, ceqsex 3489, ceqsexv 3490, ceqsex2 3492, ceqsex2v 3493, ceqsex3v 3494, ceqsex4v 3495, ceqsex6v 3496, ceqsex8v 3497, gencbvex 3498 (after changing 𝐴 = 𝑦 to 𝑦 = 𝐴), gencbvex2 3499, gencbval 3500, vtoclgft 3502 (it uses Ⅎ, whose justification nfcjust 2937 does not use ax-ext 2770) and several other vtocl* theorems (see for instance bj-vtoclg1f 34509). See also bj-ceqsaltv 34478. (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
StepHypRef Expression
1 bj-elisset 34467 . . 3 (𝐴𝑉 → ∃𝑥 𝑥 = 𝐴)
213anim3i 1151 . 2 ((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑𝜓)) ∧ 𝐴𝑉) → (Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑𝜓)) ∧ ∃𝑥 𝑥 = 𝐴))
3 bj-ceqsalt0 34475 . 2 ((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑𝜓)) ∧ ∃𝑥 𝑥 = 𝐴) → (∀𝑥(𝑥 = 𝐴𝜑) ↔ 𝜓))
42, 3syl 17 1 ((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑𝜓)) ∧ 𝐴𝑉) → (∀𝑥(𝑥 = 𝐴𝜑) ↔ 𝜓))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ w3a 1084  ∀wal 1536   = wceq 1538  ∃wex 1781  Ⅎwnf 1785   ∈ wcel 2111 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-12 2175 This theorem depends on definitions:  df-bi 210  df-an 400  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-clel 2870 This theorem is referenced by:  bj-ceqsalgALT  34481
 Copyright terms: Public domain W3C validator