Theorem elabd

Description: Explicit demonstration the class { x | ps } is not empty by the example A . (Contributed by RP, 12-Aug-2020) (Revised by AV, 23-Mar-2024)

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

Proof

Step	Hyp	Ref	Expression
1		elabd.1	|- ( ph -> A e. V )
2		elabd.2	|- ( ph -> ch )
3		elabd.3	|- ( x = A -> ( ps <-> ch ) )
4	3	elabg	|- ( A e. V -> ( A e. { x | ps } <-> ch ) )
5	1 4	syl	|- ( ph -> ( A e. { x | ps } <-> ch ) )
6	2 5	mpbird	|- ( ph -> A e. { x | ps } )