Theorem rabeqcOLD

Description: Obsolete version of rabeqc as of 15-Jan-2025. (Contributed by AV, 20-Apr-2022) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypothesis	rabeqcOLD.1	|- ( x e. A -> ph )
Assertion	rabeqcOLD	|- { x e. A | ph } = A

Proof

Step	Hyp	Ref	Expression
1		rabeqcOLD.1	|- ( x e. A -> ph )
2		df-rab	|- { x e. A | ph } = { x | ( x e. A /\ ph ) }
3		eqabcb	|- ( { x | ( x e. A /\ ph ) } = A <-> A. x ( ( x e. A /\ ph ) <-> x e. A ) )
4	1	pm4.71i	|- ( x e. A <-> ( x e. A /\ ph ) )
5	4	bicomi	|- ( ( x e. A /\ ph ) <-> x e. A )
6	3 5	mpgbir	|- { x | ( x e. A /\ ph ) } = A
7	2 6	eqtri	|- { x e. A | ph } = A