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 36069
Description: Remove from ceqsalt 3504 dependency on ax-ext 2701 (and on df-cleq 2722 and df-v 3474). Note: this is not doable with ceqsralt 3505 (or ceqsralv 3512), which uses eleq1 2819, but the same dependence removal is possible for ceqsalg 3506, ceqsal 3508, ceqsalv 3510, cgsexg 3517, cgsex2g 3518, cgsex4g 3519, ceqsex 3522, ceqsexv 3524, ceqsex2 3528, ceqsex2v 3529, ceqsex3v 3530, ceqsex4v 3531, ceqsex6v 3532, ceqsex8v 3533, gencbvex 3534 (after changing 𝐴 = 𝑦 to 𝑦 = 𝐴), gencbvex2 3535, gencbval 3536, vtoclgft 3539 (it uses , whose justification nfcjust 2882 does not use ax-ext 2701) and several other vtocl* theorems (see for instance bj-vtoclg1f 36101). See also bj-ceqsaltv 36070. (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 2813 . . 3 (𝐴𝑉 → ∃𝑥 𝑥 = 𝐴)
213anim3i 1152 . 2 ((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑𝜓)) ∧ 𝐴𝑉) → (Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑𝜓)) ∧ ∃𝑥 𝑥 = 𝐴))
3 bj-ceqsalt0 36067 . 2 ((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑𝜓)) ∧ ∃𝑥 𝑥 = 𝐴) → (∀𝑥(𝑥 = 𝐴𝜑) ↔ 𝜓))
42, 3syl 17 1 ((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑𝜓)) ∧ 𝐴𝑉) → (∀𝑥(𝑥 = 𝐴𝜑) ↔ 𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  w3a 1085  wal 1537   = wceq 1539  wex 1779  wnf 1783  wcel 2104
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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-12 2169
This theorem depends on definitions:  df-bi 206  df-an 395  df-3an 1087  df-tru 1542  df-ex 1780  df-nf 1784  df-sb 2066  df-clab 2708  df-clel 2808
This theorem is referenced by:  bj-ceqsalgALT  36073
  Copyright terms: Public domain W3C validator