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 35634
Description: Remove from ceqsalt 3504 dependency on ax-ext 2703 (and on df-cleq 2724 and df-v 3476). Note: this is not doable with ceqsralt 3505 (or ceqsralv 3512), which uses eleq1 2821, but the same dependence removal is possible for ceqsalg 3506, ceqsal 3508, ceqsalv 3510, cgsexg 3517, cgsex2g 3518, cgsex4g 3519, ceqsex 3521, ceqsexv 3523, ceqsex2 3527, ceqsex2v 3528, ceqsex3v 3529, ceqsex4v 3530, ceqsex6v 3531, ceqsex8v 3532, gencbvex 3533 (after changing 𝐴 = 𝑦 to 𝑦 = 𝐴), gencbvex2 3534, gencbval 3535, vtoclgft 3538 (it uses , whose justification nfcjust 2884 does not use ax-ext 2703) and several other vtocl* theorems (see for instance bj-vtoclg1f 35666). See also bj-ceqsaltv 35635. (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 2815 . . 3 (𝐴𝑉 → ∃𝑥 𝑥 = 𝐴)
213anim3i 1154 . 2 ((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑𝜓)) ∧ 𝐴𝑉) → (Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑𝜓)) ∧ ∃𝑥 𝑥 = 𝐴))
3 bj-ceqsalt0 35632 . 2 ((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑𝜓)) ∧ ∃𝑥 𝑥 = 𝐴) → (∀𝑥(𝑥 = 𝐴𝜑) ↔ 𝜓))
42, 3syl 17 1 ((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑𝜓)) ∧ 𝐴𝑉) → (∀𝑥(𝑥 = 𝐴𝜑) ↔ 𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  w3a 1087  wal 1539   = wceq 1541  wex 1781  wnf 1785  wcel 2106
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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-12 2171
This theorem depends on definitions:  df-bi 206  df-an 397  df-3an 1089  df-tru 1544  df-ex 1782  df-nf 1786  df-sb 2068  df-clab 2710  df-clel 2810
This theorem is referenced by:  bj-ceqsalgALT  35638
  Copyright terms: Public domain W3C validator