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	⊢ 𝐵 ∈ V
Assertion	csbex	⊢ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ∈ V

Proof

Step	Hyp	Ref	Expression
1		csbex.1	⊢ 𝐵 ∈ V
2		csbexg	⊢ ( ∀ 𝑥 𝐵 ∈ V → ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ∈ V )
3	2 1	mpg	⊢ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ∈ V