Theorem elrab3t

Description: Membership in a restricted class abstraction, using implicit substitution. (Closed theorem version of elrab3 .) (Contributed by Thierry Arnoux, 31-Aug-2017)

	Ref	Expression
Assertion	elrab3t	|- ( ( A. x ( x = A -> ( ph <-> ps ) ) /\ A e. B ) -> ( A e. { x e. B | ph } <-> ps ) )

Proof

Step	Hyp	Ref	Expression
1		df-rab	|- { x e. B | ph } = { x | ( x e. B /\ ph ) }
2	1	eleq2i	|- ( A e. { x e. B | ph } <-> A e. { x | ( x e. B /\ ph ) } )
3		id	|- ( A e. B -> A e. B )
4		nfa1	|- F/ x A. x ( x = A -> ( ph <-> ps ) )
5		nfv	|- F/ x A e. B
6	4 5	nfan	|- F/ x ( A. x ( x = A -> ( ph <-> ps ) ) /\ A e. B )
7		sp	|- ( A. x ( x = A -> ( ph <-> ps ) ) -> ( x = A -> ( ph <-> ps ) ) )
8		eleq1	|- ( x = A -> ( x e. B <-> A e. B ) )
9	8	biimparc	|- ( ( A e. B /\ x = A ) -> x e. B )
10	9	biantrurd	|- ( ( A e. B /\ x = A ) -> ( ph <-> ( x e. B /\ ph ) ) )
11	10	bibi1d	|- ( ( A e. B /\ x = A ) -> ( ( ph <-> ps ) <-> ( ( x e. B /\ ph ) <-> ps ) ) )
12	11	pm5.74da	|- ( A e. B -> ( ( x = A -> ( ph <-> ps ) ) <-> ( x = A -> ( ( x e. B /\ ph ) <-> ps ) ) ) )
13	7 12	syl5ibcom	|- ( A. x ( x = A -> ( ph <-> ps ) ) -> ( A e. B -> ( x = A -> ( ( x e. B /\ ph ) <-> ps ) ) ) )
14	13	imp	|- ( ( A. x ( x = A -> ( ph <-> ps ) ) /\ A e. B ) -> ( x = A -> ( ( x e. B /\ ph ) <-> ps ) ) )
15	6 14	alrimi	|- ( ( A. x ( x = A -> ( ph <-> ps ) ) /\ A e. B ) -> A. x ( x = A -> ( ( x e. B /\ ph ) <-> ps ) ) )
16		elabgt	|- ( ( A e. B /\ A. x ( x = A -> ( ( x e. B /\ ph ) <-> ps ) ) ) -> ( A e. { x | ( x e. B /\ ph ) } <-> ps ) )
17	3 15 16	syl2an2	|- ( ( A. x ( x = A -> ( ph <-> ps ) ) /\ A e. B ) -> ( A e. { x | ( x e. B /\ ph ) } <-> ps ) )
18	2 17	bitrid	|- ( ( A. x ( x = A -> ( ph <-> ps ) ) /\ A e. B ) -> ( A e. { x e. B | ph } <-> ps ) )