Metamath Proof Explorer

Theorem disjabso

Description: Disjointness 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	disjabso	$⊢ (Tr M \land A \in M) \to (A \cap B = \emptyset \leftrightarrow \forall x \in M (x \in A \to \neg x \in B))$

Proof

Step	Hyp	Ref	Expression
1		disj	$⊢ A \cap B = \emptyset \leftrightarrow \forall x \in A \neg x \in B$
2		ralabso	$⊢ (Tr M \land A \in M) \to (\forall x \in A \neg x \in B \leftrightarrow \forall x \in M (x \in A \to \neg x \in B))$
3	1 2	bitrid	$⊢ (Tr M \land A \in M) \to (A \cap B = \emptyset \leftrightarrow \forall x \in M (x \in A \to \neg x \in B))$