Theorem elrabrd

Description: Deduction version of elrab , just like elrabd , but backwards direction. (Contributed by Thierry Arnoux, 15-Jan-2026)

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

Proof

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