Theorem rabeq2i

Description: Inference from equality of a class variable and a restricted class abstraction. (Contributed by NM, 16-Feb-2004)

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

Proof

Step	Hyp	Ref	Expression
1		rabeq2i.1	|- A = { x e. B | ph }
2	1	eleq2i	|- ( x e. A <-> x e. { x e. B | ph } )
3		rabid	|- ( x e. { x e. B | ph } <-> ( x e. B /\ ph ) )
4	2 3	bitri	|- ( x e. A <-> ( x e. B /\ ph ) )