Theorem abbi2iOLD

Description: Obsolete version of abbi2i as of 6-May-2023. (Contributed by NM, 26-May-1993) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypothesis	abbi2iOLD.1	$$⊢x\in A\leftrightarrow \phi$$
Assertion	abbi2iOLD	$$⊢A=\left\{x|\phi \right\}$$

Proof

Step	Hyp	Ref	Expression
1		abbi2iOLD.1	$$⊢x\in A\leftrightarrow \phi$$
2		abeq2	$$⊢A=\left\{x|\phi \right\}\leftrightarrow \forall x\left(x\in A\leftrightarrow \phi \right)$$
3	2 1	mpgbir	$$⊢A=\left\{x|\phi \right\}$$