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

Theorem bj-ceqsalt 31496
 Description: Remove from ceqsalt 3072 dependency on ax-ext 2433 (and on df-cleq 2446 and df-v 3049). Note: this is not doable with ceqsralt 3073 (or ceqsralv 3078), which uses eleq1 2519, but the same dependence removal is possible for ceqsalg 3074, ceqsal 3076, ceqsalv 3077, cgsexg 3082, cgsex2g 3083, cgsex4g 3084, ceqsex 3085, ceqsexv 3086, ceqsex2 3088, ceqsex2v 3089, ceqsex3v 3090, ceqsex4v 3091, ceqsex6v 3092, ceqsex8v 3093, gencbvex 3094 (after changing to ), gencbvex2 3095, gencbval 3096, vtoclgft 3098 (it uses , whose justification nfcjust 2582 is actually provable without ax-ext 2433, as bj-nfcjust 31471 shows) and several other vtocl* theorems (see for instance bj-vtoclg1f 31530). See also bj-ceqsaltv 31497. (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 31483 . . 3
213anim3i 1197 . 2
3 bj-ceqsalt0 31494 . 2
42, 3syl 17 1
 Colors of variables: wff setvar class Syntax hints:   wi 4   wb 188   w3a 986  wal 1444   wceq 1446  wex 1665  wnf 1669   wcel 1889 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1671  ax-4 1684  ax-5 1760  ax-6 1807  ax-7 1853  ax-10 1917  ax-12 1935 This theorem depends on definitions:  df-bi 189  df-an 373  df-3an 988  df-ex 1666  df-nf 1670  df-sb 1800  df-clab 2440  df-clel 2449 This theorem is referenced by:  bj-ceqsalgALT  31500
 Copyright terms: Public domain W3C validator