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

Metamath Proof Explorer

Theorem csbprc

Description: The proper substitution of a proper class for a set into a class results in the empty set. (Contributed by NM, 17-Aug-2018) (Proof shortened by JJ, 27-Aug-2021)

		Ref	Expression
	Assertion	csbprc	$⊢ \neg A \in V \to ⦋ A / x ⦌ B = \emptyset$

Proof

Step	Hyp	Ref	Expression
1		sbcex	$⊢ \underset{˙}{[} A / x \underset{˙}{]} y \in B \to A \in V$
2		falim	$⊢ ⊥ \to A \in V$
3	1 2	pm5.21ni	$⊢ \neg A \in V \to (\underset{˙}{[} A / x \underset{˙}{]} y \in B \leftrightarrow ⊥)$
4	3	abbidv	$⊢ \neg A \in V \to \{y \| \underset{˙}{[} A / x \underset{˙}{]} y \in B\} = \{y \| ⊥\}$
5		df-csb	$⊢ ⦋ A / x ⦌ B = \{y \| \underset{˙}{[} A / x \underset{˙}{]} y \in B\}$
6		fal	$⊢ \neg ⊥$
7	6	abf	$⊢ \{y \| ⊥\} = \emptyset$
8	7	eqcomi	$⊢ \emptyset = \{y \| ⊥\}$
9	4 5 8	3eqtr4g	$⊢ \neg A \in V \to ⦋ A / x ⦌ B = \emptyset$