Theorem elrabd

Description: Membership in a restricted class abstraction, using implicit substitution. Deduction version of elrab . (Contributed by Glauco Siliprandi, 23-Oct-2021)

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

Proof

Step	Hyp	Ref	Expression
1		elrabd.1	|- ( x = A -> ( ps <-> ch ) )
2		elrabd.2	|- ( ph -> A e. B )
3		elrabd.3	|- ( ph -> ch )
4	1	elrab	|- ( A e. { x e. B | ps } <-> ( A e. B /\ ch ) )
5	2 3 4	sylanbrc	|- ( ph -> A e. { x e. B | ps } )