Theorem ceqsexg

Description: A representation of explicit substitution of a class for a variable, inferred from an implicit substitution hypothesis. (Contributed by NM, 11-Oct-2004)

	Ref	Expression
Hypotheses	ceqsexg.1	|- F/ x ps
	ceqsexg.2	|- ( x = A -> ( ph <-> ps ) )
Assertion	ceqsexg	|- ( A e. V -> ( E. x ( x = A /\ ph ) <-> ps ) )

Proof

Step	Hyp	Ref	Expression
1		ceqsexg.1	|- F/ x ps
2		ceqsexg.2	|- ( x = A -> ( ph <-> ps ) )
3		nfe1	|- F/ x E. x ( x = A /\ ph )
4	3 1	nfbi	|- F/ x ( E. x ( x = A /\ ph ) <-> ps )
5		ceqex	|- ( x = A -> ( ph <-> E. x ( x = A /\ ph ) ) )
6	5 2	bibi12d	|- ( x = A -> ( ( ph <-> ph ) <-> ( E. x ( x = A /\ ph ) <-> ps ) ) )
7		biid	|- ( ph <-> ph )
8	4 6 7	vtoclg1f	|- ( A e. V -> ( E. x ( x = A /\ ph ) <-> ps ) )