Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  onovuni Structured version   Unicode version

Theorem onovuni 7025
 Description: A variant of onfununi 7024 for operations. (Contributed by Eric Schmidt, 26-May-2009.) (Revised by Mario Carneiro, 11-Sep-2015.)
Hypotheses
Ref Expression
onovuni.1
onovuni.2
Assertion
Ref Expression
onovuni
Distinct variable groups:   ,,   ,,   ,,   ,
Allowed substitution hint:   ()

Proof of Theorem onovuni
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 onovuni.1 . . . 4
2 vex 3121 . . . . 5
3 oveq2 6303 . . . . . 6
4 eqid 2467 . . . . . 6
5 ovex 6320 . . . . . 6
63, 4, 5fvmpt 5957 . . . . 5
72, 6ax-mp 5 . . . 4
8 vex 3121 . . . . . . 7
9 oveq2 6303 . . . . . . . 8
10 ovex 6320 . . . . . . . 8
119, 4, 10fvmpt 5957 . . . . . . 7
128, 11ax-mp 5 . . . . . 6
1312a1i 11 . . . . 5
1413iuneq2i 4350 . . . 4
151, 7, 143eqtr4g 2533 . . 3
16 onovuni.2 . . . 4
1716, 12, 73sstr4g 3550 . . 3
1815, 17onfununi 7024 . 2
19 uniexg 6592 . . . 4
20 oveq2 6303 . . . . 5
21 ovex 6320 . . . . 5
2220, 4, 21fvmpt 5957 . . . 4
2319, 22syl 16 . . 3