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

Metamath Proof Explorer

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