Theorem elabgw

Description: Membership in a class abstraction, using implicit substitution and an intermediate setvar y to avoid ax-10 , ax-11 , ax-12 . It also avoids 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 -> ( ph <-> ps ) )
	elabgw.2	|- ( y = A -> ( ps <-> ch ) )
Assertion	elabgw	|- ( A e. V -> ( A e. { x | ph } <-> ch ) )

Proof

Step	Hyp	Ref	Expression
1		elabgw.1	|- ( x = y -> ( ph <-> ps ) )
2		elabgw.2	|- ( y = A -> ( ps <-> ch ) )
3		eleq1	|- ( y = A -> ( y e. { x | ph } <-> A e. { x | ph } ) )
4		df-clab	|- ( y e. { x | ph } <-> [ y / x ] ph )
5	1	sbievw	|- ( [ y / x ] ph <-> ps )
6	4 5	bitri	|- ( y e. { x | ph } <-> ps )
7	3 2 6	vtoclbg	|- ( A e. V -> ( A e. { x | ph } <-> ch ) )