Theorem elabd3

Description: Membership in a class abstraction, using implicit substitution. Deduction version of elab . (Contributed by GG, 12-Oct-2024)

	Ref	Expression
Hypotheses	elabd3.ex	|- ( ph -> A e. V )
	elabd3.is	|- ( ( ph /\ x = A ) -> ( ps <-> ch ) )
Assertion	elabd3	|- ( ph -> ( A e. { x | ps } <-> ch ) )

Proof

Step	Hyp	Ref	Expression
1		elabd3.ex	|- ( ph -> A e. V )
2		elabd3.is	|- ( ( ph /\ x = A ) -> ( ps <-> ch ) )
3		eqidd	|- ( ph -> { x | ps } = { x | ps } )
4	1 3 2	elabd2	|- ( ph -> ( A e. { x | ps } <-> ch ) )