Metamath Proof Explorer
Description: Remove from ceqsalt dependency on ax-ext (and on df-cleq and
df-v ). Note: this is not doable with ceqsralt (or ceqsralv ),
which uses eleq1 , but the same dependence removal is possible for
ceqsalg , ceqsal , ceqsalv , cgsexg , cgsex2g , cgsex4g ,
ceqsex , ceqsexv , ceqsex2 , ceqsex2v , ceqsex3v ,
ceqsex4v , ceqsex6v , ceqsex8v , gencbvex (after changing
A = y to y = A ), gencbvex2 , gencbval , vtoclgft (it uses
F/_ , whose justification nfcjust does not use ax-ext ) and
several other vtocl* theorems (see for instance bj-vtoclg1f ). See
also bj-ceqsaltv . (Contributed by BJ, 16-Jun-2019)
(Proof modification is discouraged.)
|
|
Ref |
Expression |
|
Assertion |
bj-ceqsalt |
|
Proof
Step |
Hyp |
Ref |
Expression |
1 |
|
bj-elisset |
|
2 |
1
|
3anim3i |
|
3 |
|
bj-ceqsalt0 |
|
4 |
2 3
|
syl |
|