Theorem elrab

Description: Membership in a restricted class abstraction, using implicit substitution. (Contributed by NM, 21-May-1999) Remove dependency on ax-13 . (Revised by Steven Nguyen, 23-Nov-2022)

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

Proof

Step	Hyp	Ref	Expression
1		elrab.1	|- ( x = A -> ( ph <-> ps ) )
2		elex	|- ( A e. { x e. B | ph } -> A e. _V )
3		elex	|- ( A e. B -> A e. _V )
4	3	adantr	|- ( ( A e. B /\ ps ) -> A e. _V )
5		eleq1	|- ( x = A -> ( x e. B <-> A e. B ) )
6	5 1	anbi12d	|- ( x = A -> ( ( x e. B /\ ph ) <-> ( A e. B /\ ps ) ) )
7		df-rab	|- { x e. B | ph } = { x | ( x e. B /\ ph ) }
8	6 7	elab2g	|- ( A e. _V -> ( A e. { x e. B | ph } <-> ( A e. B /\ ps ) ) )
9	2 4 8	pm5.21nii	|- ( A e. { x e. B | ph } <-> ( A e. B /\ ps ) )