# Metamath Proof Explorer

## Theorem cbvabv

Description: Rule used to change bound variables, using implicit substitution. Version of cbvab with disjoint variable conditions requiring fewer axioms. (Contributed by NM, 26-May-1999) Require x , y be disjoint to avoid ax-11 and ax-13 . (Revised by Steven Nguyen, 4-Dec-2022)

Ref Expression
Hypothesis cbvabv.1 ${⊢}{x}={y}\to \left({\phi }↔{\psi }\right)$
Assertion cbvabv ${⊢}\left\{{x}|{\phi }\right\}=\left\{{y}|{\psi }\right\}$

### Proof

Step Hyp Ref Expression
1 cbvabv.1 ${⊢}{x}={y}\to \left({\phi }↔{\psi }\right)$
2 sbco2vv ${⊢}\left[{z}/{y}\right]\left[{y}/{x}\right]{\phi }↔\left[{z}/{x}\right]{\phi }$
3 1 sbievw ${⊢}\left[{y}/{x}\right]{\phi }↔{\psi }$
4 3 sbbii ${⊢}\left[{z}/{y}\right]\left[{y}/{x}\right]{\phi }↔\left[{z}/{y}\right]{\psi }$
5 2 4 bitr3i ${⊢}\left[{z}/{x}\right]{\phi }↔\left[{z}/{y}\right]{\psi }$
6 df-clab ${⊢}{z}\in \left\{{x}|{\phi }\right\}↔\left[{z}/{x}\right]{\phi }$
7 df-clab ${⊢}{z}\in \left\{{y}|{\psi }\right\}↔\left[{z}/{y}\right]{\psi }$
8 5 6 7 3bitr4i ${⊢}{z}\in \left\{{x}|{\phi }\right\}↔{z}\in \left\{{y}|{\psi }\right\}$
9 8 eqriv ${⊢}\left\{{x}|{\phi }\right\}=\left\{{y}|{\psi }\right\}$