cbvoprab12

Description: Rule used to change first two bound variables in an operation abstraction, using implicit substitution. (Contributed by NM, 21-Feb-2004) (Proof shortened by Andrew Salmon, 22-Oct-2011)

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

Proof

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

Metamath Proof Explorer

Theorem cbvoprab12

Proof