Metamath Proof Explorer


Theorem cbvcsbw

Description: Change bound variables in a class substitution. Interestingly, this does not require any bound variable conditions on A . Version of cbvcsb with a disjoint variable condition, which does not require ax-13 . (Contributed by Jeff Hankins, 13-Sep-2009) (Revised by Gino Giotto, 10-Jan-2024)

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

Proof

Step Hyp Ref Expression
1 cbvcsbw.1 _yC
2 cbvcsbw.2 _xD
3 cbvcsbw.3 x=yC=D
4 1 nfcri yzC
5 2 nfcri xzD
6 3 eleq2d x=yzCzD
7 4 5 6 cbvsbcw [˙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