Metamath Proof Explorer

Theorem cbvoprab12v

Description: Rule used to change first two bound variables in an operation abstraction, using implicit substitution. (Contributed by NM, 8-Oct-2004)

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

Proof

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