Theorem opabidw

Description: The law of concretion. Special case of Theorem 9.5 of Quine p. 61. Version of opabid with a disjoint variable condition, which does not require ax-13 . (Contributed by NM, 14-Apr-1995) Avoid ax-13 . (Revised by GG, 26-Jan-2024)

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

Proof

Step	Hyp	Ref	Expression
1		opex	$$⊢⟨x,y⟩\in \mathrm{V}$$
2		copsexgw	$$⊢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$$