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 -> ( ph <-> ps ) )
Assertion cbvabv
|- { x | ph } = { y | ps }

Proof

Step Hyp Ref Expression
1 cbvabv.1
 |-  ( x = y -> ( ph <-> ps ) )
2 1 cbvsbv
 |-  ( [ z / x ] ph <-> [ z / y ] ps )
3 df-clab
 |-  ( z e. { x | ph } <-> [ z / x ] ph )
4 df-clab
 |-  ( z e. { y | ps } <-> [ z / y ] ps )
5 2 3 4 3bitr4i
 |-  ( z e. { x | ph } <-> z e. { y | ps } )
6 5 eqriv
 |-  { x | ph } = { y | ps }