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 ( 𝑥 = 𝑦 → ( 𝜑𝜓 ) )
Assertion cbvabv { 𝑥𝜑 } = { 𝑦𝜓 }

Proof

Step Hyp Ref Expression
1 cbvabv.1 ( 𝑥 = 𝑦 → ( 𝜑𝜓 ) )
2 1 cbvsbv ( [ 𝑧 / 𝑥 ] 𝜑 ↔ [ 𝑧 / 𝑦 ] 𝜓 )
3 df-clab ( 𝑧 ∈ { 𝑥𝜑 } ↔ [ 𝑧 / 𝑥 ] 𝜑 )
4 df-clab ( 𝑧 ∈ { 𝑦𝜓 } ↔ [ 𝑧 / 𝑦 ] 𝜓 )
5 2 3 4 3bitr4i ( 𝑧 ∈ { 𝑥𝜑 } ↔ 𝑧 ∈ { 𝑦𝜓 } )
6 5 eqriv { 𝑥𝜑 } = { 𝑦𝜓 }