Metamath Proof Explorer


Theorem ceqsalv

Description: A representation of explicit substitution of a class for a variable, inferred from an implicit substitution hypothesis. (Contributed by NM, 18-Aug-1993) Avoid ax-12 . (Revised by SN, 8-Sep-2024)

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

Proof

Step Hyp Ref Expression
1 ceqsalv.1 A V
2 ceqsalv.2 x = A φ ψ
3 19.23v x x = A ψ x x = A ψ
4 2 pm5.74i x = A φ x = A ψ
5 4 albii x x = A φ x x = A ψ
6 1 isseti x x = A
7 6 a1bi ψ x x = A ψ
8 3 5 7 3bitr4i x x = A φ ψ