Metamath Proof Explorer

Theorem n0abso

Description: Nonemptiness is absolute for transitive models. Compare Example I.16.3 of Kunen2 p. 96 and the following discussion. (Contributed by Eric Schmidt, 19-Oct-2025)

		Ref	Expression
	Assertion	n0abso	$⊢ (Tr M \land A \in M) \to (A \neq \emptyset \leftrightarrow \exists x \in M x \in A)$

Proof

Step	Hyp	Ref	Expression
1		rexabso	$⊢ (Tr M \land A \in M) \to (\exists x \in A ⊤ \leftrightarrow \exists x \in M (x \in A \land ⊤))$
2		tru	$⊢ ⊤$
3	2	rext0	$⊢ \exists x \in A ⊤ \leftrightarrow A \neq \emptyset$
4	3	bicomi	$⊢ A \neq \emptyset \leftrightarrow \exists x \in A ⊤$
5	2	biantru	$⊢ x \in A \leftrightarrow (x \in A \land ⊤)$
6	5	rexbii	$⊢ \exists x \in M x \in A \leftrightarrow \exists x \in M (x \in A \land ⊤)$
7	1 4 6	3bitr4g	$⊢ (Tr M \land A \in M) \to (A \neq \emptyset \leftrightarrow \exists x \in M x \in A)$