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 -> ( ph <-> ps ) )
	elabgw.2	|- ( y = A -> ( ps <-> ch ) )
	elab2gw.3	|- B = { x | ph }
Assertion	elab2gw	|- ( A e. V -> ( A e. B <-> ch ) )

Proof

Step	Hyp	Ref	Expression
1		elabgw.1	|- ( x = y -> ( ph <-> ps ) )
2		elabgw.2	|- ( y = A -> ( ps <-> ch ) )
3		elab2gw.3	|- B = { x | ph }
4	3	eleq2i	|- ( A e. B <-> A e. { x | ph } )
5	1 2	elabgw	|- ( A e. V -> ( A e. { x | ph } <-> ch ) )
6	4 5	syl5bb	|- ( A e. V -> ( A e. B <-> ch ) )