Metamath Proof Explorer


Theorem bj-ceqsalt

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 x ψ x x = A φ ψ A V x x = A φ ψ

Proof

Step Hyp Ref Expression
1 bj-elisset A V x x = A
2 1 3anim3i x ψ x x = A φ ψ A V x ψ x x = A φ ψ x x = A
3 bj-ceqsalt0 x ψ x x = A φ ψ x x = A x x = A φ ψ
4 2 3 syl x ψ x x = A φ ψ A V x x = A φ ψ