Metamath Proof Explorer

Theorem bj-denoteslem

Description: Lemma for bj-denotes . (Contributed by BJ, 24-Apr-2024) (Proof modification is discouraged.)

		Ref	Expression
	Assertion	bj-denoteslem	$⊢ \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 \| ⊤\}$