Theorem eqabbOLD

Description: Obsolete version of eqabb as of 12-Feb-2025. (Contributed by NM, 26-May-1993) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	eqabbOLD	|- ( A = { x | ph } <-> A. x ( x e. A <-> ph ) )

Proof

Step	Hyp	Ref	Expression
1		ax-5	|- ( y e. A -> A. x y e. A )
2		hbab1	|- ( y e. { x | ph } -> A. x y e. { x | ph } )
3	1 2	cleqh	|- ( A = { x | ph } <-> A. x ( x e. A <-> x e. { x | ph } ) )
4		abid	|- ( x e. { x | ph } <-> ph )
5	4	bibi2i	|- ( ( x e. A <-> x e. { x | ph } ) <-> ( x e. A <-> ph ) )
6	5	albii	|- ( A. x ( x e. A <-> x e. { x | ph } ) <-> A. x ( x e. A <-> ph ) )
7	3 6	bitri	|- ( A = { x | ph } <-> A. x ( x e. A <-> ph ) )