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

Metamath Proof Explorer

Theorem cbvoprab3v

Description: Rule used to change the third bound variable in an operation abstraction, using implicit substitution. (Contributed by NM, 8-Oct-2004) (Revised by David Abernethy, 19-Jun-2012)

		Ref	Expression
	Hypothesis	cbvoprab3v.1	$⊢ z = w \to (φ \leftrightarrow ψ)$
	Assertion	cbvoprab3v	$⊢ \{⟨⟨x, y⟩, z⟩ \| φ\} = \{⟨⟨x, y⟩, w⟩ \| ψ\}$

Proof

Step	Hyp	Ref	Expression
1		cbvoprab3v.1	$⊢ z = w \to (φ \leftrightarrow ψ)$
2		opeq2	$⊢ z = w \to ⟨⟨x, y⟩, z⟩ = ⟨⟨x, y⟩, w⟩$
3	2	eqeq2d	$⊢ z = w \to (v = ⟨⟨x, y⟩, z⟩ \leftrightarrow v = ⟨⟨x, y⟩, w⟩)$
4	3 1	anbi12d	$⊢ z = w \to ((v = ⟨⟨x, y⟩, z⟩ \land φ) \leftrightarrow (v = ⟨⟨x, y⟩, w⟩ \land ψ))$
5	4	cbvexvw	$⊢ \exists z (v = ⟨⟨x, y⟩, z⟩ \land φ) \leftrightarrow \exists w (v = ⟨⟨x, y⟩, w⟩ \land ψ)$
6	5	2exbii	$⊢ \exists x \exists y \exists z (v = ⟨⟨x, y⟩, z⟩ \land φ) \leftrightarrow \exists x \exists y \exists w (v = ⟨⟨x, y⟩, w⟩ \land ψ)$
7	6	abbii	$⊢ \{v \| \exists x \exists y \exists z (v = ⟨⟨x, y⟩, z⟩ \land φ)\} = \{v \| \exists x \exists y \exists w (v = ⟨⟨x, y⟩, w⟩ \land ψ)\}$
8		df-oprab	$⊢ \{⟨⟨x, y⟩, z⟩ \| φ\} = \{v \| \exists x \exists y \exists z (v = ⟨⟨x, y⟩, z⟩ \land φ)\}$
9		df-oprab	$⊢ \{⟨⟨x, y⟩, w⟩ \| ψ\} = \{v \| \exists x \exists y \exists w (v = ⟨⟨x, y⟩, w⟩ \land ψ)\}$
10	7 8 9	3eqtr4i	$⊢ \{⟨⟨x, y⟩, z⟩ \| φ\} = \{⟨⟨x, y⟩, w⟩ \| ψ\}$