Theorem opabid

Description: The law of concretion. Special case of Theorem 9.5 of Quine p. 61. Usage of this theorem is discouraged because it depends on ax-13 . Use the weaker opabidw when possible. (Contributed by NM, 14-Apr-1995) (Proof shortened by Andrew Salmon, 25-Jul-2011) (New usage is discouraged.)

	Ref	Expression
Assertion	opabid	$$⊢⟨x,y⟩\in \left\{⟨x,y⟩|\phi \right\}\leftrightarrow \phi$$

Proof

Step	Hyp	Ref	Expression
1		opex	$$⊢⟨x,y⟩\in \mathrm{V}$$
2		copsexg	$$⊢z=⟨x,y⟩\to \left(\phi \leftrightarrow \exists x\exists y\left(z=⟨x,y⟩\wedge \phi \right)\right)$$
3	2	bicomd	$$⊢z=⟨x,y⟩\to \left(\exists x\exists y\left(z=⟨x,y⟩\wedge \phi \right)\leftrightarrow \phi \right)$$
4		df-opab	$$⊢\left\{⟨x,y⟩|\phi \right\}=\left\{z|\exists x\exists y\left(z=⟨x,y⟩\wedge \phi \right)\right\}$$
5	1 3 4	elab2	$$⊢⟨x,y⟩\in \left\{⟨x,y⟩|\phi \right\}\leftrightarrow \phi$$