Theorem elab3

Description: Membership in a class abstraction using implicit substitution. (Contributed by NM, 10-Nov-2000) (Revised by AV, 16-Aug-2024)

	Ref	Expression
Hypotheses	elab3.1	|- ( ps -> A e. V )
	elab3.2	|- ( x = A -> ( ph <-> ps ) )
Assertion	elab3	|- ( A e. { x | ph } <-> ps )

Proof

Step	Hyp	Ref	Expression
1		elab3.1	|- ( ps -> A e. V )
2		elab3.2	|- ( x = A -> ( ph <-> ps ) )
3	2	elab3g	|- ( ( ps -> A e. V ) -> ( A e. { x | ph } <-> ps ) )
4	1 3	ax-mp	|- ( A e. { x | ph } <-> ps )