Metamath Proof Explorer


Theorem csb2

Description: Alternate expression for the proper substitution into a class, without referencing substitution into a wff. Note that x can be free in B but cannot occur in A . (Contributed by NM, 2-Dec-2013)

Ref Expression
Assertion csb2 A/xB=y|xx=AyB

Proof

Step Hyp Ref Expression
1 df-csb A/xB=y|[˙A/x]˙yB
2 sbc5 [˙A/x]˙yBxx=AyB
3 2 abbii y|[˙A/x]˙yB=y|xx=AyB
4 1 3 eqtri A/xB=y|xx=AyB