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

Metamath Proof Explorer

Theorem rabsssn

Description: Conditions for a restricted class abstraction to be a subset of a singleton, i.e. to be a singleton or the empty set. (Contributed by AV, 18-Apr-2019)

		Ref	Expression
	Assertion	rabsssn	$⊢ \{x \in V \| φ\} \subseteq \{X\} \leftrightarrow \forall x \in V (φ \to x = X)$

Proof

Step	Hyp	Ref	Expression
1		df-rab	$⊢ \{x \in V \| φ\} = \{x \| (x \in V \land φ)\}$
2		df-sn	$⊢ \{X\} = \{x \| x = X\}$
3	1 2	sseq12i	$⊢ \{x \in V \| φ\} \subseteq \{X\} \leftrightarrow \{x \| (x \in V \land φ)\} \subseteq \{x \| x = X\}$
4		ss2ab	$⊢ \{x \| (x \in V \land φ)\} \subseteq \{x \| x = X\} \leftrightarrow \forall x ((x \in V \land φ) \to x = X)$
5		impexp	$⊢ ((x \in V \land φ) \to x = X) \leftrightarrow (x \in V \to (φ \to x = X))$
6	5	albii	$⊢ \forall x ((x \in V \land φ) \to x = X) \leftrightarrow \forall x (x \in V \to (φ \to x = X))$
7		df-ral	$⊢ \forall x \in V (φ \to x = X) \leftrightarrow \forall x (x \in V \to (φ \to x = X))$
8	6 7	bitr4i	$⊢ \forall x ((x \in V \land φ) \to x = X) \leftrightarrow \forall x \in V (φ \to x = X)$
9	3 4 8	3bitri	$⊢ \{x \in V \| φ\} \subseteq \{X\} \leftrightarrow \forall x \in V (φ \to x = X)$