Theorem ceqsal

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 df-clab . (Revised by Wolf Lammen, 23-Jan-2025)

	Ref	Expression
Hypotheses	ceqsal.1	|- F/ x ps
	ceqsal.2	|- A e. _V
	ceqsal.3	|- ( x = A -> ( ph <-> ps ) )
Assertion	ceqsal	|- ( A. x ( x = A -> ph ) <-> ps )

Proof

Step	Hyp	Ref	Expression
1		ceqsal.1	|- F/ x ps
2		ceqsal.2	|- A e. _V
3		ceqsal.3	|- ( x = A -> ( ph <-> ps ) )
4	1	19.23	|- ( A. x ( x = A -> ps ) <-> ( E. x x = A -> ps ) )
5	3	pm5.74i	|- ( ( x = A -> ph ) <-> ( x = A -> ps ) )
6	5	albii	|- ( A. x ( x = A -> ph ) <-> A. x ( x = A -> ps ) )
7	2	isseti	|- E. x x = A
8	7	a1bi	|- ( ps <-> ( E. x x = A -> ps ) )
9	4 6 8	3bitr4i	|- ( A. x ( x = A -> ph ) <-> ps )