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 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-csb | |
|
2 | sbc5 | |
|
3 | 2 | abbii | |
4 | 1 3 | eqtri | |