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

Metamath Proof Explorer

Theorem issettru

Description: Weak version of isset . (Contributed by BJ, 24-Apr-2024)

		Ref	Expression
	Assertion	issettru	$⊢ \exists x x = A \leftrightarrow A \in \{y \| ⊤\}$

Step	Hyp	Ref	Expression
1		vextru	$⊢ x \in \{y \| ⊤\}$
2	1	biantru	$⊢ x = A \leftrightarrow (x = A \land x \in \{y \| ⊤\})$
3	2	exbii	$⊢ \exists x x = A \leftrightarrow \exists x (x = A \land x \in \{y \| ⊤\})$
4		dfclel	$⊢ A \in \{y \| ⊤\} \leftrightarrow \exists x (x = A \land x \in \{y \| ⊤\})$
5	3 4	bitr4i	$⊢ \exists x x = A \leftrightarrow A \in \{y \| ⊤\}$