Users' Mathboxes 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 36865
Description: Remove from ceqsalt 3514 dependency on ax-ext 2707 (and on df-cleq 2728 and df-v 3481). Note: this is not doable with ceqsralt 3515 (or ceqsralv 3521), which uses eleq1 2828, but the same dependence removal is possible for ceqsalg 3516, ceqsal 3518, ceqsalv 3520, cgsexg 3525, cgsex2g 3526, cgsex4g 3527, ceqsex 3529, ceqsexv 3531, ceqsex2 3534, ceqsex2v 3535, ceqsex3v 3536, ceqsex4v 3537, ceqsex6v 3538, ceqsex8v 3539, gencbvex 3540 (after changing 𝐴 = 𝑦 to 𝑦 = 𝐴), gencbvex2 3541, gencbval 3542, vtoclgft 3551 (it uses , whose justification nfcjust 2890 does not use ax-ext 2707) and several other vtocl* theorems (see for instance bj-vtoclg1f 36897). See also bj-ceqsaltv 36866. (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 elisset 2822 . . 3 (𝐴𝑉 → ∃𝑥 𝑥 = 𝐴)
213anim3i 1155 . 2 ((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑𝜓)) ∧ 𝐴𝑉) → (Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑𝜓)) ∧ ∃𝑥 𝑥 = 𝐴))
3 bj-ceqsalt0 36863 . 2 ((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑𝜓)) ∧ ∃𝑥 𝑥 = 𝐴) → (∀𝑥(𝑥 = 𝐴𝜑) ↔ 𝜓))
42, 3syl 17 1 ((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑𝜓)) ∧ 𝐴𝑉) → (∀𝑥(𝑥 = 𝐴𝜑) ↔ 𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  w3a 1087  wal 1538   = wceq 1540  wex 1779  wnf 1783  wcel 2108
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-12 2177
This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1089  df-tru 1543  df-ex 1780  df-nf 1784  df-sb 2065  df-clab 2714  df-clel 2815
This theorem is referenced by:  bj-ceqsalgALT  36869
  Copyright terms: Public domain W3C validator