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

Metamath Proof Explorer

Theorem cbvopabv

Description: Rule used to change bound variables in an ordered-pair class abstraction, using implicit substitution. (Contributed by NM, 15-Oct-1996) Reduce axiom usage. (Revised by GG, 15-Oct-2024)

		Ref	Expression
	Hypothesis	cbvopabv.1	⊢ ( ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) → ( 𝜑 ↔ 𝜓 ) )
	Assertion	cbvopabv	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } = { ⟨ 𝑧 , 𝑤 ⟩ ∣ 𝜓 }

Proof

Step	Hyp	Ref	Expression
1		cbvopabv.1	⊢ ( ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) → ( 𝜑 ↔ 𝜓 ) )
2		opeq12	⊢ ( ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) → ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑧 , 𝑤 ⟩ )
3	2	eqeq2d	⊢ ( ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) → ( 𝑣 = ⟨ 𝑥 , 𝑦 ⟩ ↔ 𝑣 = ⟨ 𝑧 , 𝑤 ⟩ ) )
4	3 1	anbi12d	⊢ ( ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) → ( ( 𝑣 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) ↔ ( 𝑣 = ⟨ 𝑧 , 𝑤 ⟩ ∧ 𝜓 ) ) )
5	4	cbvex2vw	⊢ ( ∃ 𝑥 ∃ 𝑦 ( 𝑣 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) ↔ ∃ 𝑧 ∃ 𝑤 ( 𝑣 = ⟨ 𝑧 , 𝑤 ⟩ ∧ 𝜓 ) )
6	5	abbii	⊢ { 𝑣 ∣ ∃ 𝑥 ∃ 𝑦 ( 𝑣 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) } = { 𝑣 ∣ ∃ 𝑧 ∃ 𝑤 ( 𝑣 = ⟨ 𝑧 , 𝑤 ⟩ ∧ 𝜓 ) }
7		df-opab	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } = { 𝑣 ∣ ∃ 𝑥 ∃ 𝑦 ( 𝑣 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) }
8		df-opab	⊢ { ⟨ 𝑧 , 𝑤 ⟩ ∣ 𝜓 } = { 𝑣 ∣ ∃ 𝑧 ∃ 𝑤 ( 𝑣 = ⟨ 𝑧 , 𝑤 ⟩ ∧ 𝜓 ) }
9	6 7 8	3eqtr4i	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } = { ⟨ 𝑧 , 𝑤 ⟩ ∣ 𝜓 }