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	$$⊢\left(x=w\wedge y=v\right)\to \left(\phi \leftrightarrow \psi \right)$$
Assertion	cbvoprab12v	$$⊢\left\{⟨⟨x,y⟩,z⟩|\phi \right\}=\left\{⟨⟨w,v⟩,z⟩|\psi \right\}$$

Proof

Step	Hyp	Ref	Expression
1		cbvoprab12v.1	$$⊢\left(x=w\wedge y=v\right)\to \left(\phi \leftrightarrow \psi \right)$$
2		nfv	$$⊢Ⅎw\phi$$
3		nfv	$$⊢Ⅎv\phi$$
4		nfv	$$⊢Ⅎx\psi$$
5		nfv	$$⊢Ⅎy\psi$$
6	2 3 4 5 1	cbvoprab12	$$⊢\left\{⟨⟨x,y⟩,z⟩|\phi \right\}=\left\{⟨⟨w,v⟩,z⟩|\psi \right\}$$