cbvoprab2

Description: Change the second bound variable in an operation abstraction. (Contributed by Jeff Madsen, 11-Jun-2010) (Revised by Mario Carneiro, 11-Dec-2016)

	Ref	Expression
Hypotheses	cbvoprab2.1	$⊢ Ⅎ w φ$
	cbvoprab2.2	$⊢ Ⅎ y ψ$
	cbvoprab2.3	$⊢ y = w \to (φ \leftrightarrow ψ)$
Assertion	cbvoprab2	$⊢ \{⟨⟨x, y⟩, z⟩ \| φ\} = \{⟨⟨x, w⟩, z⟩ \| ψ\}$

Proof

Step	Hyp	Ref	Expression
1		cbvoprab2.1	$⊢ Ⅎ w φ$
2		cbvoprab2.2	$⊢ Ⅎ y ψ$
3		cbvoprab2.3	$⊢ y = w \to (φ \leftrightarrow ψ)$
4		nfv	$⊢ Ⅎ w v = ⟨⟨x, y⟩, z⟩$
5	4 1	nfan	$⊢ Ⅎ w (v = ⟨⟨x, y⟩, z⟩ \land φ)$
6	5	nfex	$⊢ Ⅎ w \exists z (v = ⟨⟨x, y⟩, z⟩ \land φ)$
7		nfv	$⊢ Ⅎ y v = ⟨⟨x, w⟩, z⟩$
8	7 2	nfan	$⊢ Ⅎ y (v = ⟨⟨x, w⟩, z⟩ \land ψ)$
9	8	nfex	$⊢ Ⅎ y \exists z (v = ⟨⟨x, w⟩, z⟩ \land ψ)$
10		opeq2	$⊢ y = w \to ⟨x, y⟩ = ⟨x, w⟩$
11	10	opeq1d	$⊢ y = w \to ⟨⟨x, y⟩, z⟩ = ⟨⟨x, w⟩, z⟩$
12	11	eqeq2d	$⊢ y = w \to (v = ⟨⟨x, y⟩, z⟩ \leftrightarrow v = ⟨⟨x, w⟩, z⟩)$
13	12 3	anbi12d	$⊢ y = w \to ((v = ⟨⟨x, y⟩, z⟩ \land φ) \leftrightarrow (v = ⟨⟨x, w⟩, z⟩ \land ψ))$
14	13	exbidv	$⊢ y = w \to (\exists z (v = ⟨⟨x, y⟩, z⟩ \land φ) \leftrightarrow \exists z (v = ⟨⟨x, w⟩, z⟩ \land ψ))$
15	6 9 14	cbvexv1	$⊢ \exists y \exists z (v = ⟨⟨x, y⟩, z⟩ \land φ) \leftrightarrow \exists w \exists z (v = ⟨⟨x, w⟩, z⟩ \land ψ)$
16	15	exbii	$⊢ \exists x \exists y \exists z (v = ⟨⟨x, y⟩, z⟩ \land φ) \leftrightarrow \exists x \exists w \exists z (v = ⟨⟨x, w⟩, z⟩ \land ψ)$
17	16	abbii	$⊢ \{v \| \exists x \exists y \exists z (v = ⟨⟨x, y⟩, z⟩ \land φ)\} = \{v \| \exists x \exists w \exists z (v = ⟨⟨x, w⟩, z⟩ \land ψ)\}$
18		df-oprab	$⊢ \{⟨⟨x, y⟩, z⟩ \| φ\} = \{v \| \exists x \exists y \exists z (v = ⟨⟨x, y⟩, z⟩ \land φ)\}$
19		df-oprab	$⊢ \{⟨⟨x, w⟩, z⟩ \| ψ\} = \{v \| \exists x \exists w \exists z (v = ⟨⟨x, w⟩, z⟩ \land ψ)\}$
20	17 18 19	3eqtr4i	$⊢ \{⟨⟨x, y⟩, z⟩ \| φ\} = \{⟨⟨x, w⟩, z⟩ \| ψ\}$

Metamath Proof Explorer

Theorem cbvoprab2

Proof