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 B V
Assertion csbex A / x B V

Proof

Step Hyp Ref Expression
1 csbex.1 B V
2 csbexg x B V A / x B V
3 2 1 mpg A / x B V