Theorem elab2gw

Description: Membership in a class abstraction, using two substitution hypotheses to avoid a disjoint variable condition on x and A , which is not usually significant since B is usually a constant. (Contributed by SN, 16-May-2024)

	Ref	Expression
Hypotheses	elabgw.1	$$⊢x=y\to \left(\phi \leftrightarrow \psi \right)$$
	elabgw.2	$$⊢y=A\to \left(\psi \leftrightarrow \chi \right)$$
	elab2gw.3	$$⊢B=\left\{x|\phi \right\}$$
Assertion	elab2gw	$$⊢A\in V\to \left(A\in B\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		elab2gw.3	$$⊢B=\left\{x|\phi \right\}$$
4	3	eleq2i	$$⊢A\in B\leftrightarrow A\in \left\{x|\phi \right\}$$
5	1 2	elabgw	$$⊢A\in V\to \left(A\in \left\{x|\phi \right\}\leftrightarrow \chi \right)$$
6	4 5	bitrid	$$⊢A\in V\to \left(A\in B\leftrightarrow \chi \right)$$