This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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	⊢ { 𝑥 ∣ 𝜑 } = { 𝑦 ∣ 𝜓 }