This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 \{⟨x, y⟩ \| φ\} \leftrightarrow φ$

Proof

Step	Hyp	Ref	Expression
1		opex	$⊢ ⟨x, y⟩ \in V$
2		copsexgw	$⊢ z = ⟨x, y⟩ \to (φ \leftrightarrow \exists x \exists y (z = ⟨x, y⟩ \land φ))$
3	2	bicomd	$⊢ z = ⟨x, y⟩ \to (\exists x \exists y (z = ⟨x, y⟩ \land φ) \leftrightarrow φ)$
4		df-opab	$⊢ \{⟨x, y⟩ \| φ\} = \{z \| \exists x \exists y (z = ⟨x, y⟩ \land φ)\}$
5	1 3 4	elab2	$⊢ ⟨x, y⟩ \in \{⟨x, y⟩ \| φ\} \leftrightarrow φ$