Theorem csbex

Description: The existence of proper substitution into a class. (Contributed by NM, 7-Aug-2007) (Proof shortened by Andrew Salmon, 29-Jun-2011) (Revised by NM, 17-Aug-2018)

	Ref	Expression
Hypothesis	csbex.1	$$⊢B\in \mathrm{V}$$
Assertion	csbex	$$⊢⦋A/x⦌B\in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		csbex.1	$$⊢B\in \mathrm{V}$$
2		csbexg	$$⊢\forall xB\in \mathrm{V}\to ⦋A/x⦌B\in \mathrm{V}$$
3	2 1	mpg	$$⊢⦋A/x⦌B\in \mathrm{V}$$