Metamath Proof Explorer


Theorem ceqsexvOLD

Description: Obsolete version of ceqsexv as of 12-Oct-2024. (Contributed by NM, 2-Mar-1995) Avoid ax-12 . (Revised by Gino Giotto, 12-Oct-2024) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses ceqsexvOLD.1 A V
ceqsexvOLD.2 x = A φ ψ
Assertion ceqsexvOLD x x = A φ ψ

Proof

Step Hyp Ref Expression
1 ceqsexvOLD.1 A V
2 ceqsexvOLD.2 x = A φ ψ
3 2 biimpa x = A φ ψ
4 3 exlimiv x x = A φ ψ
5 2 biimprcd ψ x = A φ
6 5 alrimiv ψ x x = A φ
7 1 isseti x x = A
8 exintr x x = A φ x x = A x x = A φ
9 6 7 8 mpisyl ψ x x = A φ
10 4 9 impbii x x = A φ ψ