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.) |