Metamath Proof Explorer


Theorem oprabex3

Description: Existence of an operation class abstraction (special case). (Contributed by NM, 19-Oct-2004)

Ref Expression
Hypotheses oprabex3.1 H V
oprabex3.2 F = x y z | x H × H y H × H w v u f x = w v y = u f z = R
Assertion oprabex3 F V

Proof

Step Hyp Ref Expression
1 oprabex3.1 H V
2 oprabex3.2 F = x y z | x H × H y H × H w v u f x = w v y = u f z = R
3 1 1 xpex H × H V
4 moeq * z z = R
5 4 mosubop * z u f y = u f z = R
6 5 mosubop * z w v x = w v u f y = u f z = R
7 anass x = w v y = u f z = R x = w v y = u f z = R
8 7 2exbii u f x = w v y = u f z = R u f x = w v y = u f z = R
9 19.42vv u f x = w v y = u f z = R x = w v u f y = u f z = R
10 8 9 bitri u f x = w v y = u f z = R x = w v u f y = u f z = R
11 10 2exbii w v u f x = w v y = u f z = R w v x = w v u f y = u f z = R
12 11 mobii * z w v u f x = w v y = u f z = R * z w v x = w v u f y = u f z = R
13 6 12 mpbir * z w v u f x = w v y = u f z = R
14 13 a1i x H × H y H × H * z w v u f x = w v y = u f z = R
15 3 3 14 2 oprabex F V