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

Metamath Proof Explorer

Theorem rextru

Description: Two ways of expressing that a class has at least one element. (Contributed by Zhi Wang, 23-Sep-2024)

		Ref	Expression
	Assertion	rextru	$⊢ \exists x x \in A \leftrightarrow \exists x \in A ⊤$

Step	Hyp	Ref	Expression
1		tru	$⊢ ⊤$
2	1	biantru	$⊢ x \in A \leftrightarrow (x \in A \land ⊤)$
3	2	exbii	$⊢ \exists x x \in A \leftrightarrow \exists x (x \in A \land ⊤)$
4		df-rex	$⊢ \exists x \in A ⊤ \leftrightarrow \exists x (x \in A \land ⊤)$
5	3 4	bitr4i	$⊢ \exists x x \in A \leftrightarrow \exists x \in A ⊤$