Theorem elabgw

Description: Membership in a class abstraction, using two substitution hypotheses to avoid a disjoint variable condition on x and A . This is to elabg what sbievw2 is to sbievw . (Contributed by SN, 20-Apr-2024)

	Ref	Expression
Hypotheses	elabgw.1	$$⊢x=y\to \left(\phi \leftrightarrow \psi \right)$$
	elabgw.2	$$⊢y=A\to \left(\psi \leftrightarrow \chi \right)$$
Assertion	elabgw	$$⊢A\in V\to \left(A\in \left\{x|\phi \right\}\leftrightarrow \chi \right)$$

Proof

Step	Hyp	Ref	Expression
1		elabgw.1	$$⊢x=y\to \left(\phi \leftrightarrow \psi \right)$$
2		elabgw.2	$$⊢y=A\to \left(\psi \leftrightarrow \chi \right)$$
3		eleq1	$$⊢y=A\to \left(y\in \left\{x|\phi \right\}\leftrightarrow A\in \left\{x|\phi \right\}\right)$$
4		df-clab	$$⊢y\in \left\{x|\phi \right\}\leftrightarrow \left[y/x\right]\phi$$
5	1	sbievw	$$⊢\left[y/x\right]\phi \leftrightarrow \psi$$
6	4 5	bitri	$$⊢y\in \left\{x|\phi \right\}\leftrightarrow \psi$$
7	3 2 6	vtoclbg	$$⊢A\in V\to \left(A\in \left\{x|\phi \right\}\leftrightarrow \chi \right)$$