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	|- ( ( x = w /\ y = v ) -> ( ph <-> ps ) )
Assertion	cbvoprab12v	|- { <. <. x , y >. , z >. | ph } = { <. <. w , v >. , z >. | ps }

Proof

Step	Hyp	Ref	Expression
1		cbvoprab12v.1	|- ( ( x = w /\ y = v ) -> ( ph <-> ps ) )
2		nfv	|- F/ w ph
3		nfv	|- F/ v ph
4		nfv	|- F/ x ps
5		nfv	|- F/ y ps
6	2 3 4 5 1	cbvoprab12	|- { <. <. x , y >. , z >. | ph } = { <. <. w , v >. , z >. | ps }