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\to \left(\psi \leftrightarrow \chi \right)$$
	elrabd.2	$$⊢\phi \to A\in B$$
	elrabd.3	$$⊢\phi \to \chi$$
Assertion	elrabd	$$⊢\phi \to A\in \left\{x\in B|\psi \right\}$$

Proof

Step	Hyp	Ref	Expression
1		elrabd.1	$$⊢x=A\to \left(\psi \leftrightarrow \chi \right)$$
2		elrabd.2	$$⊢\phi \to A\in B$$
3		elrabd.3	$$⊢\phi \to \chi$$
4	1	elrab	$$⊢A\in \left\{x\in B|\psi \right\}\leftrightarrow \left(A\in B\wedge \chi \right)$$
5	2 3 4	sylanbrc	$$⊢\phi \to A\in \left\{x\in B|\psi \right\}$$