Metamath Proof Explorer


Theorem cbvcsb

Description: Change bound variables in a class substitution. Interestingly, this does not require any bound variable conditions on A . Usage of this theorem is discouraged because it depends on ax-13 . Use the weaker cbvcsbw when possible. (Contributed by Jeff Hankins, 13-Sep-2009) (Revised by Mario Carneiro, 11-Dec-2016) (New usage is discouraged.)

Ref Expression
Hypotheses cbvcsb.1 _yC
cbvcsb.2 _xD
cbvcsb.3 x=yC=D
Assertion cbvcsb A/xC=A/yD

Proof

Step Hyp Ref Expression
1 cbvcsb.1 _yC
2 cbvcsb.2 _xD
3 cbvcsb.3 x=yC=D
4 1 nfcri yzC
5 2 nfcri xzD
6 3 eleq2d x=yzCzD
7 4 5 6 cbvsbc [˙A/x]˙zC[˙A/y]˙zD
8 7 abbii z|[˙A/x]˙zC=z|[˙A/y]˙zD
9 df-csb A/xC=z|[˙A/x]˙zC
10 df-csb A/yD=z|[˙A/y]˙zD
11 8 9 10 3eqtr4i A/xC=A/yD