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

Metamath Proof Explorer

Theorem cbvoprab1

Description: Rule used to change first bound variable in an operation abstraction, using implicit substitution. (Contributed by NM, 20-Dec-2008) (Revised by Mario Carneiro, 5-Dec-2016)

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

Proof

Step	Hyp	Ref	Expression
1		cbvoprab1.1	$⊢ Ⅎ w φ$
2		cbvoprab1.2	$⊢ Ⅎ x ψ$
3		cbvoprab1.3	$⊢ x = w \to (φ \leftrightarrow ψ)$
4		nfv	$⊢ Ⅎ w v = ⟨x, y⟩$
5	4 1	nfan	$⊢ Ⅎ w (v = ⟨x, y⟩ \land φ)$
6	5	nfex	$⊢ Ⅎ w \exists y (v = ⟨x, y⟩ \land φ)$
7		nfv	$⊢ Ⅎ x v = ⟨w, y⟩$
8	7 2	nfan	$⊢ Ⅎ x (v = ⟨w, y⟩ \land ψ)$
9	8	nfex	$⊢ Ⅎ x \exists y (v = ⟨w, y⟩ \land ψ)$
10		opeq1	$⊢ x = w \to ⟨x, y⟩ = ⟨w, y⟩$
11	10	eqeq2d	$⊢ x = w \to (v = ⟨x, y⟩ \leftrightarrow v = ⟨w, y⟩)$
12	11 3	anbi12d	$⊢ x = w \to ((v = ⟨x, y⟩ \land φ) \leftrightarrow (v = ⟨w, y⟩ \land ψ))$
13	12	exbidv	$⊢ x = w \to (\exists y (v = ⟨x, y⟩ \land φ) \leftrightarrow \exists y (v = ⟨w, y⟩ \land ψ))$
14	6 9 13	cbvexv1	$⊢ \exists x \exists y (v = ⟨x, y⟩ \land φ) \leftrightarrow \exists w \exists y (v = ⟨w, y⟩ \land ψ)$
15	14	opabbii	$⊢ \{⟨v, z⟩ \| \exists x \exists y (v = ⟨x, y⟩ \land φ)\} = \{⟨v, z⟩ \| \exists w \exists y (v = ⟨w, y⟩ \land ψ)\}$
16		dfoprab2	$⊢ \{⟨⟨x, y⟩, z⟩ \| φ\} = \{⟨v, z⟩ \| \exists x \exists y (v = ⟨x, y⟩ \land φ)\}$
17		dfoprab2	$⊢ \{⟨⟨w, y⟩, z⟩ \| ψ\} = \{⟨v, z⟩ \| \exists w \exists y (v = ⟨w, y⟩ \land ψ)\}$
18	15 16 17	3eqtr4i	$⊢ \{⟨⟨x, y⟩, z⟩ \| φ\} = \{⟨⟨w, y⟩, z⟩ \| ψ\}$