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

Metamath Proof Explorer

Theorem cbvoprab3

Description: Rule used to change the third bound variable in an operation abstraction, using implicit substitution. (Contributed by NM, 22-Aug-2013)

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

Proof

Step	Hyp	Ref	Expression
1		cbvoprab3.1	$⊢ Ⅎ w φ$
2		cbvoprab3.2	$⊢ Ⅎ z ψ$
3		cbvoprab3.3	$⊢ z = 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	6	nfex	$⊢ Ⅎ w \exists x \exists y (v = ⟨x, y⟩ \land φ)$
8		nfv	$⊢ Ⅎ z v = ⟨x, y⟩$
9	8 2	nfan	$⊢ Ⅎ z (v = ⟨x, y⟩ \land ψ)$
10	9	nfex	$⊢ Ⅎ z \exists y (v = ⟨x, y⟩ \land ψ)$
11	10	nfex	$⊢ Ⅎ z \exists x \exists y (v = ⟨x, y⟩ \land ψ)$
12	3	anbi2d	$⊢ z = w \to ((v = ⟨x, y⟩ \land φ) \leftrightarrow (v = ⟨x, y⟩ \land ψ))$
13	12	2exbidv	$⊢ z = w \to (\exists x \exists y (v = ⟨x, y⟩ \land φ) \leftrightarrow \exists x \exists y (v = ⟨x, y⟩ \land ψ))$
14	7 11 13	cbvopab2	$⊢ \{⟨v, z⟩ \| \exists x \exists y (v = ⟨x, y⟩ \land φ)\} = \{⟨v, w⟩ \| \exists x \exists y (v = ⟨x, y⟩ \land ψ)\}$
15		dfoprab2	$⊢ \{⟨⟨x, y⟩, z⟩ \| φ\} = \{⟨v, z⟩ \| \exists x \exists y (v = ⟨x, y⟩ \land φ)\}$
16		dfoprab2	$⊢ \{⟨⟨x, y⟩, w⟩ \| ψ\} = \{⟨v, w⟩ \| \exists x \exists y (v = ⟨x, y⟩ \land ψ)\}$
17	14 15 16	3eqtr4i	$⊢ \{⟨⟨x, y⟩, z⟩ \| φ\} = \{⟨⟨x, y⟩, w⟩ \| ψ\}$