Metamath Proof Explorer


Theorem bj-ceqsalg

Description: Remove from ceqsalg dependency on ax-ext (and on df-cleq and df-v ). See also bj-ceqsalgv . (Contributed by BJ, 12-Oct-2019) (Proof modification is discouraged.)

Ref Expression
Hypotheses bj-ceqsalg.1 x ψ
bj-ceqsalg.2 x = A φ ψ
Assertion bj-ceqsalg A V x x = A φ ψ

Proof

Step Hyp Ref Expression
1 bj-ceqsalg.1 x ψ
2 bj-ceqsalg.2 x = A φ ψ
3 bj-elisset A V x x = A
4 1 2 bj-ceqsalg0 x x = A x x = A φ ψ
5 3 4 syl A V x x = A φ ψ